This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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