PowerSetWithSubst Show Code edit
thm (PowerSetWithSubst ((A x z result element)) ()
(∃ result (∀ element (↔ (∈ element result) (subst element z (∀ x (→ (∈ x z) (∈ x A)))))))
result element x A PowerSetAxiomObject
(∃ result (∀ element (↔ (∈ element result) (∀ x (→ (∈ x element) (∈ x A))))))
z element x A PowerSet-sub
(→ (= z element) (↔ (∀ x (→ (∈ x z) (∈ x A))) (∀ x (→ (∈ x element) (∈ x A)))))
makeSubstExplicit
(↔ (subst element z (∀ x (→ (∈ x z) (∈ x A)))) (∀ x (→ (∈ x element) (∈ x A))))
swapBiconditional
(↔ (∀ x (→ (∈ x element) (∈ x A))) (subst element z (∀ x (→ (∈ x z) (∈ x A)))))
(∈ element result) buildBiconditionalLL
(↔ (↔ (∈ element result) (∀ x (→ (∈ x element) (∈ x A)))) (↔ (∈ element result) (subst element z (∀ x (→ (∈ x z) (∈ x A))))))
element buildForAll
(↔ (∀ element (↔ (∈ element result) (∀ x (→ (∈ x element) (∈ x A))))) (∀ element (↔ (∈ element result) (subst element z (∀ x (→ (∈ x z) (∈ x A)))))))
result buildThereExists
(↔ (∃ result (∀ element (↔ (∈ element result) (∀ x (→ (∈ x element) (∈ x A)))))) (∃ result (∀ element (↔ (∈ element result) (subst element z (∀ x (→ (∈ x z) (∈ x A))))))))
eliminateBiconditionalReverse
(→ (∃ result (∀ element (↔ (∈ element result) (∀ x (→ (∈ x element) (∈ x A)))))) (∃ result (∀ element (↔ (∈ element result) (subst element z (∀ x (→ (∈ x z) (∈ x A))))))))
applyModusPonens
(∃ result (∀ element (↔ (∈ element result) (subst element z (∀ x (→ (∈ x z) (∈ x A)))))))
)
edit