Description: Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | unexb | ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ V ) |
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 ) |