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

Theorem opthreg 4307
 Description: Theorem for alternate representation of ordered pairs, requiring the Axiom of Set Induction ax-setind 4288 (via the preleq 4306 step). See df-op 3415 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 3506 . . . 4
3 preleq.3 . . . . 5
43prid1 3506 . . . 4
5 preleq.2 . . . . . 6
6 prexg 3974 . . . . . 6
71, 5, 6mp2an 417 . . . . 5
8 preleq.4 . . . . . 6
9 prexg 3974 . . . . . 6
103, 8, 9mp2an 417 . . . . 5
111, 7, 3, 10preleq 4306 . . . 4
122, 4, 11mpanl12 427 . . 3
13 preq1 3477 . . . . . 6
1413eqeq1d 2090 . . . . 5
155, 8preqr2 3569 . . . . 5
1614, 15syl6bi 161 . . . 4
1716imdistani 434 . . 3
1812, 17syl 14 . 2
19 preq1 3477 . . . 4