Metamath Proof Explorer


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 } ) ) )