Theorem eloni 5650

Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
eloni	⊢ (𝐴 ∈ On → Ord 𝐴)

Proof of Theorem eloni

Step	Hyp	Ref	Expression
1		elong 5648	. 2 ⊢ (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
2	1	ibi 255	1 ⊢ (𝐴 ∈ On → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 1977  Ord word 5639  Oncon0 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-uni 4373  df-tr 4681  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-on 5644

This theorem is referenced by:  onelon  5665  onin  5671  ontri1  5674  onfr  5680  onelpss  5681  onsseleq  5682  onelss  5683  ontr1  5688  ontr2  5689  ordunidif  5690  on0eln0  5697  ordsssuc  5729  onsssuc  5730  onnbtwn  5735  suc11  5748  onordi  5749  onssneli  5754  ordon  6874  ordeleqon  6880  onss  6882  ordsuc  6906  onpwsuc  6908  onpsssuc  6911  onsucmin  6913  ordunpr  6918  ordunisuc  6924  onsucuni2  6926  onuninsuci  6932  ordunisuc2  6936  ordzsl  6937  onzsl  6938  nlimon  6943  tfinds  6951  tfindsg2  6953  nnord  6965  onfununi  7325  smo11  7348  smoord  7349  smoword  7350  smogt  7351  tfrlem1  7359  tfrlem9a  7369  tfrlem15  7375  tz7.44-2  7390  tz7.48lem  7423  oe0m1  7488  oaordi  7513  oaord  7514  oacan  7515  oawordri  7517  oalimcl  7527  oaass  7528  omord2  7534  omcan  7536  omwordi  7538  omword1  7540  omword2  7541  om00  7542  omlimcl  7545  omass  7547  omeulem2  7550  omopth2  7551  oen0  7553  oeord  7555  oecan  7556  oewordi  7558  oeworde  7560  oelimcl  7567  oeeulem  7568  oeeui  7569  nnarcl  7583  nnawordi  7588  nnawordex  7604  oaabs2  7612  omabs  7614  omsmo  7621  omxpenlem  7946  infensuc  8023  onomeneq  8035  ordiso  8304  ordtypelem2  8307  hartogslem1  8330  cantnflt  8452  cantnfp1lem3  8460  cantnfp1  8461  oemapso  8462  oemapvali  8464  cantnflem1d  8468  cantnflem1  8469  cantnf  8473  oemapwe  8474  cantnffval2  8475  cnfcom  8480  r111  8521  r1ordg  8524  rankonidlem  8574  bndrank  8587  r1pw  8591  r1pwALT  8592  rankbnd2  8615  tcrank  8630  cardprclem  8688  carduni  8690  cardmin2  8707  infxpenlem  8719  alephdom  8787  alephdom2  8793  cardaleph  8795  iscard3  8799  alephfp  8814  dfac12lem1  8848  dfac12lem2  8849  dfac12lem3  8850  cflim2  8968  cofsmo  8974  cfsmolem  8975  coftr  8978  cfcof  8979  fin67  9100  hsmexlem5  9135  zorn2lem6  9206  ttukeylem3  9216  ttukeylem5  9218  ttukeylem6  9219  ttukeylem7  9220  winainflem  9394  r1limwun  9437  r1wunlim  9438  tsksuc  9463  inar1  9476  gruina  9519  grur1a  9520  grur1  9521  dfrdg2  30945  poseq  30994  soseq  30995  nodmord  31050  nodenselem5  31084  nofulllem5  31105  ontgval  31600  ontgsucval  31601  onsuctopon  31603  onintopsscon  31609  onsuct0  31610  sucneqond  32389  onsucuni3  32391  aomclem4  36645  aomclem5  36646  onfrALTlem3  37780  onfrALTlem2  37782  onfrALTlem3VD  38145  onfrALTlem2VD  38147  onsetreclem3  42249