Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  opthreg Structured version   Visualization version   Unicode version

Theorem opthreg 8141
 Description: Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 8125 (via the preleq 8140 step). See df-op 3966 for a description of other ordered pair representations. Exercise 34 of [Enderton] p. 207. (Contributed by NM, 16-Oct-1996.)
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 4071 . . . 4
3 preleq.3 . . . . 5
43prid1 4071 . . . 4
5 prex 4642 . . . . 5
6 prex 4642 . . . . 5
71, 5, 3, 6preleq 8140 . . . 4
82, 4, 7mpanl12 696 . . 3
9 preq1 4042 . . . . . 6
109eqeq1d 2473 . . . . 5
11 preleq.2 . . . . . 6
12 preleq.4 . . . . . 6
1311, 12preqr2 4141 . . . . 5
1410, 13syl6bi 236 . . . 4
1514imdistani 704 . . 3
168, 15syl 17 . 2
17 preq1 4042 . . . 4