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