Theorem 1on 8111

Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.)

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8104	. 2 ⊢ 1o = suc ∅
2		0elon 6246	. . 3 ⊢ ∅ ∈ On
3	2	onsuci 7555	. 2 ⊢ suc ∅ ∈ On
4	1, 3	eqeltri 2911	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2114  ∅c0 4293  Oncon0 6193  suc csuc 6195  1_oc1o 8097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-tr 5175  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-ord 6196  df-on 6197  df-suc 6199  df-1o 8104

This theorem is referenced by:  1oex  8112  2on  8113  ondif2  8129  2oconcl  8130  fnoe  8137  oesuclem  8152  oecl  8164  o1p1e2  8167  o2p2e4OLD  8169  om1r  8171  oe1m  8173  omword1  8201  omword2  8202  omlimcl  8206  oneo  8209  oewordi  8219  oelim2  8223  oeoa  8225  oeoe  8227  oeeui  8230  oaabs2  8274  enpr2d  8599  sucxpdom  8729  oancom  9116  cnfcom3lem  9168  pm54.43lem  9430  pm54.43  9431  infxpenc  9446  infxpenc2  9450  undjudom  9595  endjudisj  9596  djuen  9597  dju1p1e2  9601  dju1p1e2ALT  9602  xpdjuen  9607  mapdjuen  9608  djuxpdom  9613  djufi  9614  djuinf  9616  infdju1  9617  pwdju1  9618  pwdjudom  9640  isfin4p1  9739  pwxpndom2  10089  wunex2  10162  wuncval2  10171  tsk2  10189  efgmnvl  18842  frgpnabllem1  18995  dmdprdpr  19173  dprdpr  19174  psr1crng  20357  psr1assa  20358  psr1tos  20359  psr1bas  20361  vr1cl2  20363  ply1lss  20366  ply1subrg  20367  ressply1bas2  20398  ressply1add  20400  ressply1mul  20401  ressply1vsca  20402  subrgply1  20403  ply1plusgfvi  20412  psr1ring  20417  psr1lmod  20419  psr1sca  20420  ply1ascl  20428  subrg1ascl  20429  subrg1asclcl  20430  subrgvr1  20431  subrgvr1cl  20432  coe1z  20433  coe1mul2lem1  20437  coe1mul2  20439  coe1tm  20443  evls1val  20485  evls1rhm  20487  evls1sca  20488  evl1val  20494  evl1rhm  20497  evl1sca  20499  evl1var  20501  evls1var  20503  mpfpf1  20516  pf1mpf  20517  pf1ind  20520  xkofvcn  22294  xpstopnlem1  22419  ufildom1  22536  deg1z  24683  deg1addle  24697  deg1vscale  24700  deg1vsca  24701  deg1mulle2  24705  deg1le0  24707  ply1nzb  24718  sltval2  33165  noextendlt  33178  sltsolem1  33182  nosepnelem  33186  nolt02o  33201  rankeq1o  33634  ssoninhaus  33798  onint1  33799  1oequni2o  34651  finxp1o  34675  finxpreclem3  34676  finxpreclem4  34677  finxpreclem5  34678  finxpsuclem  34680  pw2f1ocnv  39641  wepwsolem  39649  pwfi2f1o  39703  sn1dom  39899  pr2dom  39900  tr3dom  39901  clsk1indlem4  40401  ply1ass23l  44443