Theorem omelon 8840

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 8837	. 2 ⊢ ω ∈ V
2		omelon2 7355	. 2 ⊢ (ω ∈ V → ω ∈ On)
3	1, 2	ax-mp 5	1 ⊢ ω ∈ On

Syntax hints:   ∈ wcel 2107  Vcvv 3398  Oncon0 5976  ωcom 7343

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 5017  ax-nul 5025  ax-pr 5138  ax-un 7226  ax-inf2 8835

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 4672  df-br 4887  df-opab 4949  df-tr 4988  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-om 7344

This theorem is referenced by:  oancom  8845  cnfcomlem  8893  cnfcom  8894  cnfcom2lem  8895  cnfcom2  8896  cnfcom3lem  8897  cnfcom3  8898  cnfcom3clem  8899  cardom  9145  infxpenlem  9169  xpomen  9171  infxpidm2  9173  infxpenc  9174  infxpenc2lem1  9175  infxpenc2  9178  alephon  9225  infenaleph  9247  iunfictbso  9270  dfac12k  9304  infunsdom1  9370  domtriomlem  9599  iunctb  9731  pwcfsdom  9740  canthp1lem2  9810  pwfseqlem4a  9818  pwfseqlem4  9819  pwfseqlem5  9820  wunex3  9898  znnen  15345  qnnen  15346  cygctb  18679  2ndcctbss  21667  2ndcomap  21670  2ndcsep  21671  tx1stc  21862  tx2ndc  21863  met1stc  22734  met2ndci  22735  re2ndc  23012  uniiccdif  23782  dyadmbl  23804  opnmblALT  23807  mbfimaopnlem  23859  aannenlem3  24522  poimirlem32  34069  numinfctb  38636