This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union Introduce the Axiom of Union unexgOLD
Description: Obsolete version of unexg as of 21-Jul-2025. (Contributed by NM , 18-Sep-2006) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Assertion
unexgOLD ⊢ A ∈ V ∧ B ∈ W → A ∪ B ∈ V
Proof
Step
Hyp
Ref
Expression
1
elex ⊢ A ∈ V → A ∈ V
2
elex ⊢ B ∈ W → B ∈ V
3
unexb ⊢ A ∈ V ∧ B ∈ V ↔ A ∪ B ∈ V
4
3
biimpi ⊢ A ∈ V ∧ B ∈ V → A ∪ B ∈ V
5
1 2 4
syl2an ⊢ A ∈ V ∧ B ∈ W → A ∪ B ∈ V