Theorem 1on 8092

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 8085	. 2 ⊢ 1o = suc ∅
2		0elon 6212	. . 3 ⊢ ∅ ∈ On
3	2	onsuci 7533	. 2 ⊢ suc ∅ ∈ On
4	1, 3	eqeltri 2886	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2111  ∅c0 4243  Oncon0 6159  suc csuc 6161  1_oc1o 8078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-tr 5137  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-ord 6162  df-on 6163  df-suc 6165  df-1o 8085

This theorem is referenced by:  1oex  8093  2on  8094  ondif2  8110  2oconcl  8111  fnoe  8118  oesuclem  8133  oecl  8145  o1p1e2  8148  o2p2e4OLD  8150  om1r  8152  oe1m  8154  omword1  8182  omword2  8183  omlimcl  8187  oneo  8190  oewordi  8200  oelim2  8204  oeoa  8206  oeoe  8208  oeeui  8211  oaabs2  8255  enpr2d  8580  sucxpdom  8711  oancom  9098  cnfcom3lem  9150  pm54.43lem  9413  pm54.43  9414  infxpenc  9429  infxpenc2  9433  undjudom  9578  endjudisj  9579  djuen  9580  dju1p1e2  9584  dju1p1e2ALT  9585  xpdjuen  9590  mapdjuen  9591  djuxpdom  9596  djufi  9597  djuinf  9599  infdju1  9600  pwdju1  9601  pwdjudom  9627  isfin4p1  9726  pwxpndom2  10076  wunex2  10149  wuncval2  10158  tsk2  10176  efgmnvl  18832  frgpnabllem1  18986  dmdprdpr  19164  dprdpr  19165  psr1crng  20816  psr1assa  20817  psr1tos  20818  psr1bas  20820  vr1cl2  20822  ply1lss  20825  ply1subrg  20826  ressply1bas2  20857  ressply1add  20859  ressply1mul  20860  ressply1vsca  20861  subrgply1  20862  ply1plusgfvi  20871  psr1ring  20876  psr1lmod  20878  psr1sca  20879  ply1ascl  20887  subrg1ascl  20888  subrg1asclcl  20889  subrgvr1  20890  subrgvr1cl  20891  coe1z  20892  coe1mul2lem1  20896  coe1mul2  20898  coe1tm  20902  evls1val  20944  evls1rhm  20946  evls1sca  20947  evl1val  20953  evl1rhm  20956  evl1sca  20958  evl1var  20960  evls1var  20962  mpfpf1  20975  pf1mpf  20976  pf1ind  20979  xkofvcn  22289  xpstopnlem1  22414  ufildom1  22531  deg1z  24688  deg1addle  24702  deg1vscale  24705  deg1vsca  24706  deg1mulle2  24710  deg1le0  24712  ply1nzb  24723  sltval2  33276  noextendlt  33289  sltsolem1  33293  nosepnelem  33297  nolt02o  33312  rankeq1o  33745  ssoninhaus  33909  onint1  33910  1oequni2o  34785  finxp1o  34809  finxpreclem3  34810  finxpreclem4  34811  finxpreclem5  34812  finxpsuclem  34814  pw2f1ocnv  39978  wepwsolem  39986  pwfi2f1o  40040  sn1dom  40234  pr2dom  40235  tr3dom  40236  clsk1indlem4  40747  ply1ass23l  44790