Theorem eloni 5733

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 5731	. 2 ⊢ (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
2	1	ibi 256	1 ⊢ (𝐴 ∈ On → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 1990  Ord word 5722  Oncon0 5723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-uni 4437  df-tr 4753  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726  df-on 5727

This theorem is referenced by:  onelon  5748  onin  5754  ontri1  5757  onfr  5763  onelpss  5764  onsseleq  5765  onelss  5766  ontr1  5771  ontr2  5772  ordunidif  5773  on0eln0  5780  ordsssuc  5812  onsssuc  5813  onnbtwn  5818  suc11  5831  onordi  5832  onssneli  5837  ordon  6982  ordeleqon  6988  onss  6990  ordsuc  7014  onpwsuc  7016  onpsssuc  7019  onsucmin  7021  ordunpr  7026  ordunisuc  7032  onsucuni2  7034  onuninsuci  7040  ordunisuc2  7044  ordzsl  7045  onzsl  7046  nlimon  7051  tfinds  7059  tfindsg2  7061  nnord  7073  onfununi  7438  smo11  7461  smoord  7462  smoword  7463  smogt  7464  tfrlem1  7472  tfrlem9a  7482  tfrlem15  7488  tz7.44-2  7503  tz7.48lem  7536  oe0m1  7601  oaordi  7626  oaord  7627  oacan  7628  oawordri  7630  oalimcl  7640  oaass  7641  omord2  7647  omcan  7649  omwordi  7651  omword1  7653  omword2  7654  om00  7655  omlimcl  7658  omass  7660  omeulem2  7663  omopth2  7664  oen0  7666  oeord  7668  oecan  7669  oewordi  7671  oeworde  7673  oelimcl  7680  oeeulem  7681  oeeui  7682  nnarcl  7696  nnawordi  7701  nnawordex  7717  oaabs2  7725  omabs  7727  omsmo  7734  omxpenlem  8061  infensuc  8138  onomeneq  8150  ordiso  8421  ordtypelem2  8424  hartogslem1  8447  cantnflt  8569  cantnfp1lem3  8577  cantnfp1  8578  oemapso  8579  oemapvali  8581  cantnflem1d  8585  cantnflem1  8586  cantnf  8590  oemapwe  8591  cantnffval2  8592  cnfcom  8597  r111  8638  r1ordg  8641  rankonidlem  8691  bndrank  8704  r1pw  8708  r1pwALT  8709  rankbnd2  8732  tcrank  8747  cardprclem  8805  carduni  8807  cardmin2  8824  infxpenlem  8836  alephdom  8904  alephdom2  8910  cardaleph  8912  iscard3  8916  alephfp  8931  dfac12lem1  8965  dfac12lem2  8966  dfac12lem3  8967  cflim2  9085  cofsmo  9091  cfsmolem  9092  coftr  9095  cfcof  9096  fin67  9217  hsmexlem5  9252  zorn2lem6  9323  ttukeylem3  9333  ttukeylem5  9335  ttukeylem6  9336  ttukeylem7  9337  winainflem  9515  r1limwun  9558  r1wunlim  9559  tsksuc  9584  inar1  9597  gruina  9640  grur1a  9641  grur1  9642  dfrdg2  31701  poseq  31750  soseq  31751  nodmord  31806  noextendseq  31820  noextenddif  31821  nosupno  31849  nosupres  31853  noetalem3  31865  ontgval  32430  ontgsucval  32431  onsuctopon  32433  onintopssconn  32439  onsuct0  32440  sucneqond  33213  onsucuni3  33215  aomclem4  37627  aomclem5  37628  onfrALTlem3  38759  onfrALTlem2  38761  onfrALTlem3VD  39123  onfrALTlem2VD  39125  onsetreclem3  42450