Union Show Code edit
thm (Union ((A x) (B x)) ()
(↔ (∈ B (⋃ A)) (∃ x (∧ (∈ B x) (∈ x A))))
A z x′ UnionAsAbstraction
(= (⋃ A) (abstract z (∃ x′ (∧ (∈ z x′) (∈ x′ A)))))
B buildMembershipLL
(↔ (∈ B (⋃ A)) (∈ B (abstract z (∃ x′ (∧ (∈ z x′) (∈ x′ A))))))
B z x′ A x UnionObject
(↔ (∈ B (abstract z (∃ x′ (∧ (∈ z x′) (∈ x′ A))))) (∃ x (∧ (∈ B x) (∈ x A))))
applyBiconditionalTransitivity
(↔ (∈ B (⋃ A)) (∃ x (∧ (∈ B x) (∈ x A))))
)
edit