PowerSetObject Show Code edit
thm (PowerSetObject ((B x) (A x z x′)) ()
(↔ (∈ B (abstract z (∀ x′ (→ (∈ x′ z) (∈ x′ A))))) (∀ x (→ (∈ x B) (∈ x A))))
z y x A PowerSet-sub
(→ (= z y) (↔ (∀ x (→ (∈ x z) (∈ x A))) (∀ x (→ (∈ x y) (∈ x A)))))
x z A x′ PowerSet-changeVariable
(↔ (∀ x (→ (∈ x z) (∈ x A))) (∀ x′ (→ (∈ x′ z) (∈ x′ A))))
transformImplicationBiconditionalLeft
(→ (= z y) (↔ (∀ x′ (→ (∈ x′ z) (∈ x′ A))) (∀ x (→ (∈ x y) (∈ x A)))))
y B x A PowerSet-sub
(→ (= y B) (↔ (∀ x (→ (∈ x y) (∈ x A))) (∀ x (→ (∈ x B) (∈ x A)))))
result y x A PowerSetAxiomObject
(∃ result (∀ y (↔ (∈ y result) (∀ x (→ (∈ x y) (∈ x A))))))
SetObject
(↔ (∈ B (abstract z (∀ x′ (→ (∈ x′ z) (∈ x′ A))))) (∀ x (→ (∈ x B) (∈ x A))))
)
edit