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∈V
opthreg.2 ⊢B∈V
opthreg.3 ⊢C∈V
opthreg.4 ⊢D∈V
Assertion opthreg ⊢AAB=CCD↔A=C∧B=D

Proof

Step Hyp Ref Expression
1 opthreg.1 ⊢A∈V
2 opthreg.2 ⊢B∈V
3 opthreg.3 ⊢C∈V
4 opthreg.4 ⊢D∈V
5 1 prid1 ⊢A∈AB
6 3 prid1 ⊢C∈CD
7 prex ⊢AB∈V
8 7 preleq ⊢A∈AB∧C∈CD∧AAB=CCD→A=C∧AB=CD
9 5 6 8 mpanl12 ⊢AAB=CCD→A=C∧AB=CD
10 preq1 ⊢A=C→AB=CB
11 10 eqeq1d ⊢A=C→AB=CD↔CB=CD
12 2 4 preqr2 ⊢CB=CD→B=D
13 11 12 syl6bi ⊢A=C→AB=CD→B=D
14 13 imdistani ⊢A=C∧AB=CD→A=C∧B=D
15 9 14 syl ⊢AAB=CCD→A=C∧B=D
16 preq1 ⊢A=C→AAB=CAB
17 16 adantr ⊢A=C∧B=D→AAB=CAB
18 preq12 ⊢A=C∧B=D→AB=CD
19 18 preq2d ⊢A=C∧B=D→CAB=CCD
20 17 19 eqtrd ⊢A=C∧B=D→AAB=CCD
21 15 20 impbii ⊢AAB=CCD↔A=C∧B=D