SubsetReflexivity Show Code edit
thm (SubsetReflexivity () () (⊆ A A)
A EqualityReflexivity
(= A A)
A A EqualitySubset
(↔ (= A A) (∧ (⊆ A A) (⊆ A A)))
eliminateBiconditionalReverse
(→ (= A A) (∧ (⊆ A A) (⊆ A A)))
applyModusPonens
(∧ (⊆ A A) (⊆ A A))
conflateConjunction
(⊆ A A)
)
edit