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	⊢ 𝐴 ∈ V
	opthw.2	⊢ 𝐵 ∈ V
Assertion	uniop	⊢ ∪ ⟨ 𝐴 , 𝐵 ⟩ = { 𝐴 , 𝐵 }

Proof

Step	Hyp	Ref	Expression
1		opthw.1	⊢ 𝐴 ∈ V
2		opthw.2	⊢ 𝐵 ∈ V
3	1 2	dfop	⊢ ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } }
4	3	unieqi	⊢ ∪ ⟨ 𝐴 , 𝐵 ⟩ = ∪ { { 𝐴 } , { 𝐴 , 𝐵 } }
5		snex	⊢ { 𝐴 } ∈ V
6		prex	⊢ { 𝐴 , 𝐵 } ∈ V
7	5 6	unipr	⊢ ∪ { { 𝐴 } , { 𝐴 , 𝐵 } } = ( { 𝐴 } ∪ { 𝐴 , 𝐵 } )
8		snsspr1	⊢ { 𝐴 } ⊆ { 𝐴 , 𝐵 }
9		ssequn1	⊢ ( { 𝐴 } ⊆ { 𝐴 , 𝐵 } ↔ ( { 𝐴 } ∪ { 𝐴 , 𝐵 } ) = { 𝐴 , 𝐵 } )
10	8 9	mpbi	⊢ ( { 𝐴 } ∪ { 𝐴 , 𝐵 } ) = { 𝐴 , 𝐵 }
11	4 7 10	3eqtri	⊢ ∪ ⟨ 𝐴 , 𝐵 ⟩ = { 𝐴 , 𝐵 }