Metamath Proof Explorer


Theorem unexb

Description: Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998)

Ref Expression
Assertion unexb ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 unexg ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴𝐵 ) ∈ V )
2 ssun1 𝐴 ⊆ ( 𝐴𝐵 )
3 ssexg ( ( 𝐴 ⊆ ( 𝐴𝐵 ) ∧ ( 𝐴𝐵 ) ∈ V ) → 𝐴 ∈ V )
4 2 3 mpan ( ( 𝐴𝐵 ) ∈ V → 𝐴 ∈ V )
5 ssun2 𝐵 ⊆ ( 𝐴𝐵 )
6 ssexg ( ( 𝐵 ⊆ ( 𝐴𝐵 ) ∧ ( 𝐴𝐵 ) ∈ V ) → 𝐵 ∈ V )
7 5 6 mpan ( ( 𝐴𝐵 ) ∈ V → 𝐵 ∈ V )
8 4 7 jca ( ( 𝐴𝐵 ) ∈ V → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
9 1 8 impbii ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴𝐵 ) ∈ V )