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 ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)↔{A}\cup {B}\in \mathrm{V}$

Proof

Step Hyp Ref Expression
1 uneq1 ${⊢}{x}={A}\to {x}\cup {y}={A}\cup {y}$
2 1 eleq1d ${⊢}{x}={A}\to \left({x}\cup {y}\in \mathrm{V}↔{A}\cup {y}\in \mathrm{V}\right)$
3 uneq2 ${⊢}{y}={B}\to {A}\cup {y}={A}\cup {B}$
4 3 eleq1d ${⊢}{y}={B}\to \left({A}\cup {y}\in \mathrm{V}↔{A}\cup {B}\in \mathrm{V}\right)$
5 vex ${⊢}{x}\in \mathrm{V}$
6 vex ${⊢}{y}\in \mathrm{V}$
7 5 6 unex ${⊢}{x}\cup {y}\in \mathrm{V}$
8 2 4 7 vtocl2g ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to {A}\cup {B}\in \mathrm{V}$
9 ssun1 ${⊢}{A}\subseteq {A}\cup {B}$
10 ssexg ${⊢}\left({A}\subseteq {A}\cup {B}\wedge {A}\cup {B}\in \mathrm{V}\right)\to {A}\in \mathrm{V}$
11 9 10 mpan ${⊢}{A}\cup {B}\in \mathrm{V}\to {A}\in \mathrm{V}$
12 ssun2 ${⊢}{B}\subseteq {A}\cup {B}$
13 ssexg ${⊢}\left({B}\subseteq {A}\cup {B}\wedge {A}\cup {B}\in \mathrm{V}\right)\to {B}\in \mathrm{V}$
14 12 13 mpan ${⊢}{A}\cup {B}\in \mathrm{V}\to {B}\in \mathrm{V}$
15 11 14 jca ${⊢}{A}\cup {B}\in \mathrm{V}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
16 8 15 impbii ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)↔{A}\cup {B}\in \mathrm{V}$