This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uniop

Description: The union of an ordered pair. Theorem 65 of Suppes p. 39. (Contributed by NM, 17-Aug-2004) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses opthw.1 ⊢ A ∈ V
opthw.2 ⊢ B ∈ V
Assertion uniop ⊢ ⋃ A B = A B

Proof

Step Hyp Ref Expression
1 opthw.1 ⊢ A ∈ V
2 opthw.2 ⊢ B ∈ V
3 1 2 dfop ⊢ A B = A A B
4 3 unieqi ⊢ ⋃ A B = ⋃ A A B
5 snex ⊢ A ∈ V
6 prex ⊢ A B ∈ V
7 5 6 unipr ⊢ ⋃ A A B = A ∪ A B
8 snsspr1 ⊢ A ⊆ A B
9 ssequn1 ⊢ A ⊆ A B ↔ A ∪ A B = A B
10 8 9 mpbi ⊢ A ∪ A B = A B
11 4 7 10 3eqtri ⊢ ⋃ A B = A B