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		unexg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
2		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
3		ssexg	⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → 𝐴 ∈ V )
4	2 3	mpan	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → 𝐴 ∈ V )
5		ssun2	⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
6		ssexg	⊢ ( ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → 𝐵 ∈ V )
7	5 6	mpan	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → 𝐵 ∈ V )
8	4 7	jca	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
9	1 8	impbii	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ V )