UnionObject Show Code edit
thm (UnionObject ((B x) (A x z x′)) ()
(↔ (∈ B (abstract z (∃ x′ (∧ (∈ z x′) (∈ x′ A))))) (∃ x (∧ (∈ B x) (∈ x A))))
z y x A Union-sub
(→ (= z y) (↔ (∃ x (∧ (∈ z x) (∈ x A))) (∃ x (∧ (∈ y x) (∈ x A)))))
x z A x′ Union-changeVariable
(↔ (∃ x (∧ (∈ z x) (∈ x A))) (∃ x′ (∧ (∈ z x′) (∈ x′ A))))
transformImplicationBiconditionalLeft
(→ (= z y) (↔ (∃ x′ (∧ (∈ z x′) (∈ x′ A))) (∃ x (∧ (∈ y x) (∈ x A)))))
y B x A Union-sub
(→ (= y B) (↔ (∃ x (∧ (∈ y x) (∈ x A))) (∃ x (∧ (∈ B x) (∈ x A)))))
result y x A UnionAxiomObject
(∃ result (∀ y (↔ (∈ y result) (∃ x (∧ (∈ y x) (∈ x A))))))
SetObject
(↔ (∈ B (abstract z (∃ x′ (∧ (∈ z x′) (∈ x′ A))))) (∃ x (∧ (∈ B x) (∈ x A))))
)
edit