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

Theorem opthwiener 4702
 Description: Justification theorem for the ordered pair definition in Norbert Wiener, "A simplification of the logic of relations," Proc. of the Cambridge Philos. Soc., 1914, vol. 17, pp.387-390. It is also shown as a definition in [Enderton] p. 36 and as Exercise 4.8(b) of [Mendelson] p. 230. It is meaningful only for classes that exist as sets (i.e. are not proper classes). See df-op 3974 for other ordered pair definitions. (Contributed by NM, 28-Sep-2003.)
Hypotheses
Ref Expression
opthw.1
opthw.2
Assertion
Ref Expression
opthwiener

Proof of Theorem opthwiener
StepHypRef Expression
1 id 22 . . . . . . 7
2 snex 4640 . . . . . . . . . . . 12
32prid2 4080 . . . . . . . . . . 11
4 eleq2 2517 . . . . . . . . . . 11
53, 4mpbii 215 . . . . . . . . . 10
62elpr 3985 . . . . . . . . . 10
75, 6sylib 200 . . . . . . . . 9
8 0ex 4534 . . . . . . . . . . . . 13
98prid2 4080 . . . . . . . . . . . 12
10 opthw.2 . . . . . . . . . . . . . 14
1110snnz 4089 . . . . . . . . . . . . 13
128elsnc 3991 . . . . . . . . . . . . . 14
13 eqcom 2457 . . . . . . . . . . . . . 14
1412, 13bitri 253 . . . . . . . . . . . . 13
1511, 14nemtbir 2718 . . . . . . . . . . . 12
16 nelneq2 2553 . . . . . . . . . . . 12
179, 15, 16mp2an 677 . . . . . . . . . . 11
18 eqcom 2457 . . . . . . . . . . 11
1917, 18mtbi 300 . . . . . . . . . 10
20 biorf 407 . . . . . . . . . 10
2119, 20ax-mp 5 . . . . . . . . 9
227, 21sylibr 216 . . . . . . . 8
2322preq2d 4057 . . . . . . 7
241, 23eqtr4d 2487 . . . . . 6
25 prex 4641 . . . . . . 7
26 prex 4641 . . . . . . 7
2725, 26preqr1 4147 . . . . . 6
2824, 27syl 17 . . . . 5
29 snex 4640 . . . . . 6
30 snex 4640 . . . . . 6
3129, 30preqr1 4147 . . . . 5
3228, 31syl 17 . . . 4
33 opthw.1 . . . . 5
3433sneqr 4138 . . . 4
3532, 34syl 17 . . 3
36 snex 4640 . . . . . 6
3736sneqr 4138 . . . . 5
3822, 37syl 17 . . . 4
3910sneqr 4138 . . . 4
4038, 39syl 17 . . 3
4135, 40jca 535 . 2
42 sneq 3977 . . . . 5
4342preq1d 4056 . . . 4
4443preq1d 4056 . . 3
45 sneq 3977 . . . . 5
46 sneq 3977 . . . . 5
4745, 46syl 17 . . . 4
4847preq2d 4057 . . 3
4944, 48sylan9eq 2504 . 2
5041, 49impbii 191 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wb 188   wo 370   wa 371   wceq 1443   wcel 1886  cvv 3044  c0 3730  csn 3967  cpr 3969 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-v 3046  df-dif 3406  df-un 3408  df-nul 3731  df-sn 3968  df-pr 3970 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator