Theorem omelon 9495

Description: Omega is an ordinal number. (Contributed by NM, 10-May-1998.) (Revised by Mario Carneiro, 30-Jan-2013.)

Assertion

Ref	Expression
omelon	⊢ ω ∈ On

Proof of Theorem omelon

Step	Hyp	Ref	Expression
1		omex 9492	. 2 ⊢ ω ∈ V
2		omelon2 7785	. 2 ⊢ (ω ∈ V → ω ∈ On)
3	1, 2	ax-mp 5	1 ⊢ ω ∈ On

Syntax hints:   ∈ wcel 2105  Vcvv 3441  Oncon0 6296  ωcom 7772

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pr 5369  ax-un 7642  ax-inf2 9490

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-tr 5207  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-om 7773

This theorem is referenced by:  oancom  9500  cnfcomlem  9548  cnfcom  9549  cnfcom2lem  9550  cnfcom2  9551  cnfcom3lem  9552  cnfcom3  9553  cnfcom3clem  9554  cardom  9835  infxpenlem  9862  xpomen  9864  infxpidm2  9866  infxpenc  9867  infxpenc2lem1  9868  infxpenc2  9871  alephon  9918  infenaleph  9940  iunfictbso  9963  dfac12k  9996  infunsdom1  10062  domtriomlem  10291  iunctb  10423  pwcfsdom  10432  canthp1lem2  10502  pwfseqlem4a  10510  pwfseqlem4  10511  pwfseqlem5  10512  wunex3  10590  znnen  16012  qnnen  16013  cygctb  19580  2ndcctbss  22704  2ndcomap  22707  2ndcsep  22708  tx1stc  22899  tx2ndc  22900  met1stc  23775  met2ndci  23776  re2ndc  24062  uniiccdif  24840  dyadmbl  24862  opnmblALT  24865  mbfimaopnlem  24917  aannenlem3  25588  exrecfnlem  35648  poimirlem32  35907  numinfctb  41179  nnawordexg  41301  dflim5  41303  oacl2g  41304  omabs2  41305  omcl2  41306  ofoaf  41309  ofoafo  41310  naddcnff  41316  naddcnffo  41318  naddcnfcom  41320  naddcnfid1  41321  naddcnfid2  41322  naddcnfass  41323  infordmin  41449  minregex  41451  omiscard  41460  sucomisnotcard  41461  aleph1min  41474  alephiso3  41476