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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
Proof
Step
Hyp
Ref
Expression
1
elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2
elex ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
3
unexb ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ V )
4
3
biimpi ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
5
1 2 4
syl2an ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )