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