HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem opthreg 6732
Description: Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 6719 (via the preleq 6731 step). See df-op 3277 for a description of other ordered pair representations. Exercise 34 of [Enderton] p. 207.
Hypotheses
Ref Expression
preleq.1
preleq.2
preleq.3
preleq.4
Assertion
Ref Expression
opthreg

Proof of Theorem opthreg
StepHypRef Expression
1 preleq.1 . . . . 5
21prid1 3354 . . . 4
3 preleq.3 . . . . 5
43prid1 3354 . . . 4
5 prex 3759 . . . . 5
6 prex 3759 . . . . 5
71, 5, 3, 6preleq 6731 . . . 4
82, 4, 7mpanl12 658 . . 3
9 preq1 3329 . . . . . 6
109eqeq1d 2098 . . . . 5
11 preleq.2 . . . . . 6
12 preleq.4 . . . . . 6
1311, 12preqr2 3399 . . . . 5
1410, 13syl6bi 217 . . . 4
1514imdistani 667 . . 3
168, 15syl 15 . 2
17 preq1 3329 . . . 4
1817adantr 444 . . 3
19 preq12 3331 . . . 4
2019preq2d 3336 . . 3
2118, 20eqtrd 2122 . 2
2216, 21impbii 178 1
Colors of variables: wff set class
Syntax hints:   wb 174   wa 357   wceq 1531   wcel 1533  cvv 2500  cpr 3269
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687  ax-nul 3696  ax-pr 3756  ax-reg 6719
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-rab 2306  df-v 2502  df-sbc 2669  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3086  df-if 3195  df-sn 3274  df-pr 3275  df-op 3277  df-br 3592  df-opab 3645  df-eprel 3844  df-fr 3891
Copyright terms: Public domain