Theorem 1on 7454

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

Assertion

Ref	Expression
1on	⊢ 1𝑜 ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 7447	. 2 ⊢ 1𝑜 = suc ∅
2		0elon 5695	. . 3 ⊢ ∅ ∈ On
3	2	onsuci 6930	. 2 ⊢ suc ∅ ∈ On
4	1, 3	eqeltri 2684	1 ⊢ 1𝑜 ∈ On

Syntax hints:   ∈ wcel 1977  ∅c0 3874  Oncon0 5640  suc csuc 5642  1_𝑜c1o 7440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-on 5644  df-suc 5646  df-1o 7447

This theorem is referenced by:  2on  7455  ondif2  7469  2oconcl  7470  fnoe  7477  oev  7481  oe0  7489  oev2  7490  oesuclem  7492  oecl  7504  o1p1e2  7507  o2p2e4  7508  om1r  7510  oe1m  7512  omword1  7540  omword2  7541  omlimcl  7545  oneo  7548  oewordi  7558  oelim2  7562  oeoa  7564  oeoe  7566  oeeui  7569  oaabs2  7612  endisj  7932  sdom1  8045  sucxpdom  8054  oancom  8431  cnfcom3lem  8483  pm54.43lem  8708  pm54.43  8709  infxpenc  8724  infxpenc2  8728  uncdadom  8876  cdaun  8877  cdaen  8878  cda1dif  8881  pm110.643  8882  pm110.643ALT  8883  cdacomen  8886  cdaassen  8887  xpcdaen  8888  mapcdaen  8889  cdaxpdom  8894  cdafi  8895  cdainf  8897  infcda1  8898  pwcda1  8899  pwcdadom  8921  cfsuc  8962  isfin4-3  9020  dcomex  9152  pwcfsdom  9284  pwxpndom2  9366  wunex2  9439  wuncval2  9448  tsk2  9466  sadcf  15013  sadcp1  15015  xpscg  16041  xpscfn  16042  xpsc0  16043  xpsc1  16044  xpsfrnel  16046  xpsfrnel2  16048  xpsle  16064  efgmnvl  17950  efgi1  17957  frgpuptinv  18007  frgpnabllem1  18099  dmdprdpr  18271  dprdpr  18272  psr1crng  19378  psr1assa  19379  psr1tos  19380  psr1bas  19382  vr1cl2  19384  ply1lss  19387  ply1subrg  19388  coe1fval3  19399  ressply1bas2  19419  ressply1add  19421  ressply1mul  19422  ressply1vsca  19423  subrgply1  19424  00ply1bas  19431  ply1plusgfvi  19433  psr1ring  19438  psr1lmod  19440  psr1sca  19441  ply1ascl  19449  subrg1ascl  19450  subrg1asclcl  19451  subrgvr1  19452  subrgvr1cl  19453  coe1z  19454  coe1mul2lem1  19458  coe1mul2  19460  coe1tm  19464  evls1val  19506  evls1rhm  19508  evls1sca  19509  evl1val  19514  evl1rhm  19517  evl1sca  19519  evl1var  19521  evls1var  19523  mpfpf1  19536  pf1mpf  19537  pf1ind  19540  xkofvcn  21297  xpstopnlem1  21422  xpstopnlem2  21424  ufildom1  21540  xpsdsval  21996  deg1z  23651  deg1addle  23665  deg1vscale  23668  deg1vsca  23669  deg1mulle2  23673  deg1le0  23675  ply1nzb  23686  sltval2  31053  nofv  31054  noxp1o  31063  sltsolem1  31067  bdayfo  31074  nobnddown  31100  rankeq1o  31448  ssoninhaus  31617  onint1  31618  finxp1o  32405  finxpreclem3  32406  finxpreclem4  32407  finxpreclem5  32408  finxpsuclem  32410  pw2f1ocnv  36622  wepwsolem  36630  pwfi2f1o  36684  clsk3nimkb  37358  clsk1indlem4  37362  clsk1indlem1  37363  ply1ass23l  41964