UnorderedPairAsAbstraction Show Code edit
defthm (UnorderedPairAsAbstraction object (unorderedPair A B) ((A y) (B y)) ()
(= (unorderedPair A B) (abstract y (∨ (= y A) (= y B))))
# We need to prove { x | x = A ∨ x = B } = { y | y = A ∨ y = B }.
result element x A B UnorderedPairWithSubst
(∃ result (∀ element (↔ (∈ element result) (subst element x (∨ (= x A) (= x B))))))
result element y A B UnorderedPairWithSubst
(∃ result (∀ element (↔ (∈ element result) (subst element y (∨ (= y A) (= y B))))))
x y A B UnorderedPair-sub
(→ (= x y) (↔ (∨ (= x A) (= x B)) (∨ (= y A) (= y B))))
ChangeVariableAbstraction
(= (abstract x (∨ (= x A) (= x B))) (abstract y (∨ (= y A) (= y B))))
)
edit