Theorem 1on 8274

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 8267	. 2 ⊢ 1o = suc ∅
2		0elon 6304	. . 3 ⊢ ∅ ∈ On
3	2	onsuci 7660	. 2 ⊢ suc ∅ ∈ On
4	1, 3	eqeltri 2835	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2108  ∅c0 4253  Oncon0 6251  suc csuc 6253  1_oc1o 8260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-11 2156  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-tr 5188  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-ord 6254  df-on 6255  df-suc 6257  df-1o 8267

This theorem is referenced by:  2on  8275  1oexOLD  8281  ondif2  8294  2oconcl  8295  fnoe  8302  oesuclem  8317  oecl  8329  o1p1e2  8332  o2p2e4OLD  8334  om1r  8336  oe1m  8338  omword1  8366  omword2  8367  omlimcl  8371  oneo  8374  oewordi  8384  oelim2  8388  oeoa  8390  oeoe  8392  oeeui  8395  oaabs2  8439  enpr2d  8792  sucxpdom  8961  oancom  9339  cnfcom3lem  9391  pm54.43lem  9689  pm54.43  9690  infxpenc  9705  infxpenc2  9709  undjudom  9854  endjudisj  9855  djuen  9856  dju1p1e2  9860  dju1p1e2ALT  9861  xpdjuen  9866  mapdjuen  9867  djuxpdom  9872  djufi  9873  djuinf  9875  infdju1  9876  pwdju1  9877  pwdjudom  9903  isfin4p1  10002  pwxpndom2  10352  wunex2  10425  wuncval2  10434  tsk2  10452  efgmnvl  19235  frgpnabllem1  19389  dmdprdpr  19567  dprdpr  19568  psr1crng  21268  psr1assa  21269  psr1tos  21270  psr1bas  21272  vr1cl2  21274  ply1lss  21277  ply1subrg  21278  ressply1bas2  21309  ressply1add  21311  ressply1mul  21312  ressply1vsca  21313  subrgply1  21314  ply1plusgfvi  21323  psr1ring  21328  psr1lmod  21330  psr1sca  21331  ply1ascl  21339  subrg1ascl  21340  subrg1asclcl  21341  subrgvr1  21342  subrgvr1cl  21343  coe1z  21344  coe1mul2lem1  21348  coe1mul2  21350  coe1tm  21354  evls1val  21396  evls1rhm  21398  evls1sca  21399  evl1val  21405  evl1rhm  21408  evl1sca  21410  evl1var  21412  evls1var  21414  mpfpf1  21427  pf1mpf  21428  pf1ind  21431  xkofvcn  22743  xpstopnlem1  22868  ufildom1  22985  deg1z  25157  deg1addle  25171  deg1vscale  25174  deg1vsca  25175  deg1mulle2  25179  deg1le0  25181  ply1nzb  25192  ssttrcl  33701  ttrcltr  33702  dmttrcl  33707  ttrclselem2  33712  sltval2  33786  noextendlt  33799  sltsolem1  33805  nosepnelem  33809  nolt02o  33825  rankeq1o  34400  ssoninhaus  34564  onint1  34565  1oequni2o  35466  finxp1o  35490  finxpreclem3  35491  finxpreclem4  35492  finxpreclem5  35493  finxpsuclem  35495  pw2f1ocnv  40775  wepwsolem  40783  pwfi2f1o  40837  sn1dom  41031  pr2dom  41032  tr3dom  41033  clsk1indlem4  41543  ply1ass23l  45611