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 e. _V
	opthw.2	|- B e. _V
Assertion	uniop	|- U. <. A , B >. = { A , B }

Proof

Step	Hyp	Ref	Expression
1		opthw.1	|- A e. _V
2		opthw.2	|- B e. _V
3	1 2	dfop	|- <. A , B >. = { { A } , { A , B } }
4	3	unieqi	|- U. <. A , B >. = U. { { A } , { A , B } }
5		snex	|- { A } e. _V
6		prex	|- { A , B } e. _V
7	5 6	unipr	|- U. { { A } , { A , B } } = ( { A } u. { A , B } )
8		snsspr1	|- { A } C_ { A , B }
9		ssequn1	|- ( { A } C_ { A , B } <-> ( { A } u. { A , B } ) = { A , B } )
10	8 9	mpbi	|- ( { A } u. { A , B } ) = { A , B }
11	4 7 10	3eqtri	|- U. <. A , B >. = { A , B }