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