Theorem opeqpr

Description: Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	opeqpr.1	|- A e. _V
	opeqpr.2	|- B e. _V
	opeqpr.3	|- C e. _V
	opeqpr.4	|- D e. _V
Assertion	opeqpr	|- ( <. A , B >. = { C , D } <-> ( ( C = { A } /\ D = { A , B } ) \/ ( C = { A , B } /\ D = { A } ) ) )

Proof

Step	Hyp	Ref	Expression
1		opeqpr.1	|- A e. _V
2		opeqpr.2	|- B e. _V
3		opeqpr.3	|- C e. _V
4		opeqpr.4	|- D e. _V
5		eqcom	|- ( <. A , B >. = { C , D } <-> { C , D } = <. A , B >. )
6	1 2	dfop	|- <. A , B >. = { { A } , { A , B } }
7	6	eqeq2i	|- ( { C , D } = <. A , B >. <-> { C , D } = { { A } , { A , B } } )
8		snex	|- { A } e. _V
9		prex	|- { A , B } e. _V
10	3 4 8 9	preq12b	|- ( { C , D } = { { A } , { A , B } } <-> ( ( C = { A } /\ D = { A , B } ) \/ ( C = { A , B } /\ D = { A } ) ) )
11	5 7 10	3bitri	|- ( <. A , B >. = { C , D } <-> ( ( C = { A } /\ D = { A , B } ) \/ ( C = { A , B } /\ D = { A } ) ) )