Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  opthreg Unicode version

Theorem opthreg 4280
 Description: Theorem for alternate representation of ordered pairs, requiring the Axiom of Set Induction ax-setind 4262 (via the preleq 4279 step). See df-op 3384 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 3476 . . . 4
3 preleq.3 . . . . 5
43prid1 3476 . . . 4
5 preleq.2 . . . . . 6
6 prexgOLD 3946 . . . . . 6
71, 5, 6mp2an 402 . . . . 5
8 preleq.4 . . . . . 6
9 prexgOLD 3946 . . . . . 6
103, 8, 9mp2an 402 . . . . 5
111, 7, 3, 10preleq 4279 . . . 4
122, 4, 11mpanl12 412 . . 3
13 preq1 3447 . . . . . 6
1413eqeq1d 2048 . . . . 5
155, 8preqr2 3540 . . . . 5
1614, 15syl6bi 152 . . . 4
1716imdistani 419 . . 3
1812, 17syl 14 . 2
19 preq1 3447 . . . 4