UnionAsAbstraction Show Code edit
defthm (UnionAsAbstraction object (⋃ A) ((A x z)) ()
(= (⋃ A) (abstract z (∃ x (∧ (∈ z x) (∈ x A)))))
result element z′ x′ A UnionWithSubst
(∃ result (∀ element (↔ (∈ element result) (subst element z′ (∃ x′ (∧ (∈ z′ x′) (∈ x′ A)))))))
result element z x A UnionWithSubst
(∃ result (∀ element (↔ (∈ element result) (subst element z (∃ x (∧ (∈ z x) (∈ x A)))))))
z′ z x A Union-sub
(→ (= z′ z) (↔ (∃ x (∧ (∈ z′ x) (∈ x A))) (∃ x (∧ (∈ z x) (∈ x A)))))
x z′ A x′ Union-changeVariable
(↔ (∃ x (∧ (∈ z′ x) (∈ x A))) (∃ x′ (∧ (∈ z′ x′) (∈ x′ A))))
transformImplicationBiconditionalLeft
(→ (= z′ z) (↔ (∃ x′ (∧ (∈ z′ x′) (∈ x′ A))) (∃ x (∧ (∈ z x) (∈ x A)))))
ChangeVariableAbstraction
(= (abstract z′ (∃ x′ (∧ (∈ z′ x′) (∈ x′ A)))) (abstract z (∃ x (∧ (∈ z x) (∈ x A)))))
)
edit