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 
|- ( ( A e. _V /\ B e. _V ) <-> ( A u. B ) e. _V )

Proof

Step Hyp Ref Expression
1 uneq1 
 |-  ( x = A -> ( x u. y ) = ( A u. y ) )
2 1 eleq1d 
 |-  ( x = A -> ( ( x u. y ) e. _V <-> ( A u. y ) e. _V ) )
3 uneq2 
 |-  ( y = B -> ( A u. y ) = ( A u. B ) )
4 3 eleq1d 
 |-  ( y = B -> ( ( A u. y ) e. _V <-> ( A u. B ) e. _V ) )
5 vex 
 |-  x e. _V
6 vex 
 |-  y e. _V
7 5 6 unex 
 |-  ( x u. y ) e. _V
8 2 4 7 vtocl2g 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A u. B ) e. _V )
9 ssun1 
 |-  A C_ ( A u. B )
10 ssexg 
 |-  ( ( A C_ ( A u. B ) /\ ( A u. B ) e. _V ) -> A e. _V )
11 9 10 mpan 
 |-  ( ( A u. B ) e. _V -> A e. _V )
12 ssun2 
 |-  B C_ ( A u. B )
13 ssexg 
 |-  ( ( B C_ ( A u. B ) /\ ( A u. B ) e. _V ) -> B e. _V )
14 12 13 mpan 
 |-  ( ( A u. B ) e. _V -> B e. _V )
15 11 14 jca 
 |-  ( ( A u. B ) e. _V -> ( A e. _V /\ B e. _V ) )
16 8 15 impbii 
 |-  ( ( A e. _V /\ B e. _V ) <-> ( A u. B ) e. _V )