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		uneq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∪ 𝑦 ) = ( 𝐴 ∪ 𝑦 ) )
2	1	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∪ 𝑦 ) ∈ V ↔ ( 𝐴 ∪ 𝑦 ) ∈ V ) )
3		uneq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∪ 𝑦 ) = ( 𝐴 ∪ 𝐵 ) )
4	3	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∪ 𝑦 ) ∈ V ↔ ( 𝐴 ∪ 𝐵 ) ∈ V ) )
5		vex	⊢ 𝑥 ∈ V
6		vex	⊢ 𝑦 ∈ V
7	5 6	unex	⊢ ( 𝑥 ∪ 𝑦 ) ∈ V
8	2 4 7	vtocl2g	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
9		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
10		ssexg	⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → 𝐴 ∈ V )
11	9 10	mpan	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → 𝐴 ∈ V )
12		ssun2	⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
13		ssexg	⊢ ( ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → 𝐵 ∈ V )
14	12 13	mpan	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → 𝐵 ∈ V )
15	11 14	jca	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
16	8 15	impbii	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ V )