PowerSet Show Code edit
thm (PowerSet () () (↔ (∈ B (power A)) (⊆ B A))
B A x PowerSetForAll
(↔ (∈ B (power A)) (∀ x (→ (∈ x B) (∈ x A))))
B A x Subset
(↔ (⊆ B A) (∀ x (→ (∈ x B) (∈ x A))))
swapBiconditional
(↔ (∀ x (→ (∈ x B) (∈ x A))) (⊆ B A))
applyBiconditionalTransitivity
(↔ (∈ B (power A)) (⊆ B A))
)
edit