UnionWithSubst Show Code edit
thm (UnionWithSubst ((A x z result element)) ()
(∃ result (∀ element (↔ (∈ element result) (subst element z (∃ x (∧ (∈ z x) (∈ x A)))))))
result element x A UnionAxiomObject
(∃ result (∀ element (↔ (∈ element result) (∃ x (∧ (∈ element x) (∈ x A))))))
z element x A Union-sub
(→ (= z element) (↔ (∃ x (∧ (∈ z x) (∈ x A))) (∃ x (∧ (∈ element x) (∈ x A)))))
makeSubstExplicit
(↔ (subst element z (∃ x (∧ (∈ z x) (∈ x A)))) (∃ x (∧ (∈ element x) (∈ x A))))
swapBiconditional
(↔ (∃ x (∧ (∈ element x) (∈ x A))) (subst element z (∃ x (∧ (∈ z x) (∈ x A)))))
(∈ element result) buildBiconditionalLL
(↔ (↔ (∈ element result) (∃ x (∧ (∈ element x) (∈ x A)))) (↔ (∈ element result) (subst element z (∃ x (∧ (∈ z x) (∈ x A))))))
element buildForAll
(↔ (∀ element (↔ (∈ element result) (∃ x (∧ (∈ element x) (∈ x A))))) (∀ element (↔ (∈ element result) (subst element z (∃ x (∧ (∈ z x) (∈ x A)))))))
result buildThereExists
(↔ (∃ result (∀ element (↔ (∈ element result) (∃ x (∧ (∈ element x) (∈ x A)))))) (∃ result (∀ element (↔ (∈ element result) (subst element z (∃ x (∧ (∈ z x) (∈ x A))))))))
eliminateBiconditionalReverse
(→ (∃ result (∀ element (↔ (∈ element result) (∃ x (∧ (∈ element x) (∈ x A)))))) (∃ result (∀ element (↔ (∈ element result) (subst element z (∃ x (∧ (∈ z x) (∈ x A))))))))
applyModusPonens
(∃ result (∀ element (↔ (∈ element result) (subst element z (∃ x (∧ (∈ z x) (∈ x A)))))))
)
edit