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∈V∧B∈V↔A∪B∈V

Proof

Step Hyp Ref Expression
1 uneq1 ⊢x=A→x∪y=A∪y
2 1 eleq1d ⊢x=A→x∪y∈V↔A∪y∈V
3 uneq2 ⊢y=B→A∪y=A∪B
4 3 eleq1d ⊢y=B→A∪y∈V↔A∪B∈V
5 vex ⊢x∈V
6 vex ⊢y∈V
7 5 6 unex ⊢x∪y∈V
8 2 4 7 vtocl2g ⊢A∈V∧B∈V→A∪B∈V
9 ssun1 ⊢A⊆A∪B
10 ssexg ⊢A⊆A∪B∧A∪B∈V→A∈V
11 9 10 mpan ⊢A∪B∈V→A∈V
12 ssun2 ⊢B⊆A∪B
13 ssexg ⊢B⊆A∪B∧A∪B∈V→B∈V
14 12 13 mpan ⊢A∪B∈V→B∈V
15 11 14 jca ⊢A∪B∈V→A∈V∧B∈V
16 8 15 impbii ⊢A∈V∧B∈V↔A∪B∈V