Theorem 1on 7852

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 7845	. 2 ⊢ 1o = suc ∅
2		0elon 6031	. . 3 ⊢ ∅ ∈ On
3	2	onsuci 7318	. 2 ⊢ suc ∅ ∈ On
4	1, 3	eqeltri 2855	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2107  ∅c0 4141  Oncon0 5978  suc csuc 5980  1_oc1o 7838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pr 5140  ax-un 7228

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-tr 4990  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-ord 5981  df-on 5982  df-suc 5984  df-1o 7845

This theorem is referenced by:  1oex  7853  2on  7854  ondif2  7868  2oconcl  7869  fnoe  7876  oesuclem  7891  oecl  7903  o1p1e2  7906  o2p2e4  7907  om1r  7909  oe1m  7911  omword1  7939  omword2  7940  omlimcl  7944  oneo  7947  oewordi  7957  oelim2  7961  oeoa  7963  oeoe  7965  oeeui  7968  oaabs2  8011  sucxpdom  8459  oancom  8847  cnfcom3lem  8899  pm54.43lem  9160  pm54.43  9161  infxpenc  9176  infxpenc2  9180  uncdadom  9330  cdaun  9331  cdaen  9332  cda1dif  9335  pm110.643  9336  pm110.643ALT  9337  cdacomen  9340  cdaassen  9341  xpcdaen  9342  mapcdaen  9343  cdaxpdom  9348  cdafi  9349  cdainf  9351  infcda1  9352  pwcda1  9353  pwcdadom  9375  isfin4-3  9474  pwxpndom2  9824  wunex2  9897  wuncval2  9906  tsk2  9924  xpscg  16608  xpscfn  16609  xpsc1  16611  efgmnvl  18515  frgpnabllem1  18666  dmdprdpr  18839  dprdpr  18840  psr1crng  19957  psr1assa  19958  psr1tos  19959  psr1bas  19961  vr1cl2  19963  ply1lss  19966  ply1subrg  19967  ressply1bas2  19998  ressply1add  20000  ressply1mul  20001  ressply1vsca  20002  subrgply1  20003  ply1plusgfvi  20012  psr1ring  20017  psr1lmod  20019  psr1sca  20020  ply1ascl  20028  subrg1ascl  20029  subrg1asclcl  20030  subrgvr1  20031  subrgvr1cl  20032  coe1z  20033  coe1mul2lem1  20037  coe1mul2  20039  coe1tm  20043  evls1val  20085  evls1rhm  20087  evls1sca  20088  evl1val  20093  evl1rhm  20096  evl1sca  20098  evl1var  20100  evls1var  20102  mpfpf1  20115  pf1mpf  20116  pf1ind  20119  xkofvcn  21900  xpstopnlem1  22025  ufildom1  22142  deg1z  24288  deg1addle  24302  deg1vscale  24305  deg1vsca  24306  deg1mulle2  24310  deg1le0  24312  ply1nzb  24323  sltval2  32402  noextendlt  32415  sltsolem1  32419  nosepnelem  32423  nolt02o  32438  rankeq1o  32871  ssoninhaus  33034  onint1  33035  1oequni2o  33814  finxp1o  33827  finxpreclem3  33828  finxpreclem4  33829  finxpreclem5  33830  finxpsuclem  33832  pw2f1ocnv  38573  wepwsolem  38581  pwfi2f1o  38635  clsk1indlem4  39308  ply1ass23l  43195