Theorem dfpr2

Description: Alternate definition of unordered pair. Definition 5.1 of TakeutiZaring p. 15. (Contributed by NM, 24-Apr-1994)

	Ref	Expression
Assertion	dfpr2	|- { A , B } = { x | ( x = A \/ x = B ) }

Proof

Step	Hyp	Ref	Expression
1		df-pr	|- { A , B } = ( { A } u. { B } )
2		elun	|- ( x e. ( { A } u. { B } ) <-> ( x e. { A } \/ x e. { B } ) )
3		velsn	|- ( x e. { A } <-> x = A )
4		velsn	|- ( x e. { B } <-> x = B )
5	3 4	orbi12i	|- ( ( x e. { A } \/ x e. { B } ) <-> ( x = A \/ x = B ) )
6	2 5	bitri	|- ( x e. ( { A } u. { B } ) <-> ( x = A \/ x = B ) )
7	6	abbi2i	|- ( { A } u. { B } ) = { x | ( x = A \/ x = B ) }
8	1 7	eqtri	|- { A , B } = { x | ( x = A \/ x = B ) }