UnorderedPairWithSubst Show Code edit
thm (UnorderedPairWithSubst ((A x result element) (B x result element)) ()
(∃ result (∀ element (↔ (∈ element result) (subst element x (∨ (= x A) (= x B))))))
result element A B PairingObject
(∃ result (∀ element (↔ (∈ element result) (∨ (= element A) (= element B)))))
x element A B UnorderedPair-sub
(→ (= x element) (↔ (∨ (= x A) (= x B)) (∨ (= element A) (= element B))))
makeSubstExplicit
(↔ (subst element x (∨ (= x A) (= x B))) (∨ (= element A) (= element B)))
swapBiconditional
(↔ (∨ (= element A) (= element B)) (subst element x (∨ (= x A) (= x B))))
(∈ element result) buildBiconditionalLL
(↔ (↔ (∈ element result) (∨ (= element A) (= element B))) (↔ (∈ element result) (subst element x (∨ (= x A) (= x B)))))
element buildForAll
(↔ (∀ element (↔ (∈ element result) (∨ (= element A) (= element B)))) (∀ element (↔ (∈ element result) (subst element x (∨ (= x A) (= x B))))))
result buildThereExists
(↔ (∃ result (∀ element (↔ (∈ element result) (∨ (= element A) (= element B))))) (∃ result (∀ element (↔ (∈ element result) (subst element x (∨ (= x A) (= x B)))))))
eliminateBiconditionalReverse
(→ (∃ result (∀ element (↔ (∈ element result) (∨ (= element A) (= element B))))) (∃ result (∀ element (↔ (∈ element result) (subst element x (∨ (= x A) (= x B)))))))
applyModusPonens
(∃ result (∀ element (↔ (∈ element result) (subst element x (∨ (= x A) (= x B))))))
)
edit