ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0elon Structured version   GIF version

Theorem 0elon 4074
Description: The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.)
Assertion
Ref Expression
0elon On

Proof of Theorem 0elon
StepHypRef Expression
1 ord0 4073 . 2 Ord ∅
2 0ex 3854 . . 3 V
32elon 4056 . 2 (∅ On ↔ Ord ∅)
41, 3mpbir 134 1 On
Colors of variables: wff set class
Syntax hints:   wcel 1370  c0 3197  Ord word 4044  Oncon0 4045
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-nul 3853
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-dif 2893  df-in 2897  df-ss 2904  df-nul 3198  df-pw 3332  df-uni 3551  df-tr 3825  df-iord 4048  df-on 4050
This theorem is referenced by:  inton  4075  onn0  4082  onm  4083  limon  4184  ordtriexmid  4190  ordtri2orexmid  4191  onsucsssucexmid  4192  onsucelsucexmid  4195  ordsoexmid  4220  ordpwsucexmid  4226  rdgi0g  5882  rdg0  5891  frec0g  5898  1on  5919  ordgt0ge1  5929  omv  5946  oa0  5948  om0  5949  oei0  5950  omcl  5952  omv2  5956  oaword1  5961  nna0r  5968  nnm0r  5969
  Copyright terms: Public domain W3C validator