PowerSetForAll Show Code edit
thm (PowerSetForAll ((A x) (B x)) ()
(↔ (∈ B (power A)) (∀ x (→ (∈ x B) (∈ x A))))
A z x′ PowerSetAsAbstraction
(= (power A) (abstract z (∀ x′ (→ (∈ x′ z) (∈ x′ A)))))
B buildMembershipLL
(↔ (∈ B (power A)) (∈ B (abstract z (∀ x′ (→ (∈ x′ z) (∈ x′ A))))))
B z x′ A x PowerSetObject
(↔ (∈ B (abstract z (∀ x′ (→ (∈ x′ z) (∈ x′ A))))) (∀ x (→ (∈ x B) (∈ x A))))
applyBiconditionalTransitivity
(↔ (∈ B (power A)) (∀ x (→ (∈ x B) (∈ x A))))
)
edit