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

Metamath Proof Explorer

Theorem opthreg

Description: Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg (via the preleq step). See df-op for a description of other ordered pair representations. Exercise 34 of Enderton p. 207. (Contributed by NM, 16-Oct-1996) (Proof shortened by AV, 15-Jun-2022)

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

Proof

Step Hyp Ref Expression
1 opthreg.1 
 |-  A e. _V
2 opthreg.2 
 |-  B e. _V
3 opthreg.3 
 |-  C e. _V
4 opthreg.4 
 |-  D e. _V
5 1 prid1 
 |-  A e. { A , B }
6 3 prid1 
 |-  C e. { C , D }
7 prex 
 |-  { A , B } e. _V
8 7 preleq 
 |-  ( ( ( A e. { A , B } /\ C e. { C , D } ) /\ { A , { A , B } } = { C , { C , D } } ) -> ( A = C /\ { A , B } = { C , D } ) )
9 5 6 8 mpanl12 
 |-  ( { A , { A , B } } = { C , { C , D } } -> ( A = C /\ { A , B } = { C , D } ) )
10 preq1 
 |-  ( A = C -> { A , B } = { C , B } )
11 10 eqeq1d 
 |-  ( A = C -> ( { A , B } = { C , D } <-> { C , B } = { C , D } ) )
12 2 4 preqr2 
 |-  ( { C , B } = { C , D } -> B = D )
13 11 12 biimtrdi 
 |-  ( A = C -> ( { A , B } = { C , D } -> B = D ) )
14 13 imdistani 
 |-  ( ( A = C /\ { A , B } = { C , D } ) -> ( A = C /\ B = D ) )
15 9 14 syl 
 |-  ( { A , { A , B } } = { C , { C , D } } -> ( A = C /\ B = D ) )
16 preq1 
 |-  ( A = C -> { A , { A , B } } = { C , { A , B } } )
17 16 adantr 
 |-  ( ( A = C /\ B = D ) -> { A , { A , B } } = { C , { A , B } } )
18 preq12 
 |-  ( ( A = C /\ B = D ) -> { A , B } = { C , D } )
19 18 preq2d 
 |-  ( ( A = C /\ B = D ) -> { C , { A , B } } = { C , { C , D } } )
20 17 19 eqtrd 
 |-  ( ( A = C /\ B = D ) -> { A , { A , B } } = { C , { C , D } } )
21 15 20 impbii 
 |-  ( { A , { A , B } } = { C , { C , D } } <-> ( A = C /\ B = D ) )