Theorem eloni 6201

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ord word 6190  Oncon0 6191

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-v 3496  df-in 3943  df-ss 3952  df-uni 4839  df-tr 5173  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-ord 6194  df-on 6195

This theorem is referenced by:  onelon  6216  onin  6222  ontri1  6225  onfr  6230  onelpss  6231  onsseleq  6232  onelss  6233  ontr1  6237  ontr2  6238  ordunidif  6239  on0eln0  6246  ordsssuc  6277  onsssuc  6278  onnbtwn  6282  suc11  6294  onordi  6295  onssneli  6300  epweon  7497  ordeleqon  7503  onss  7505  ordsuc  7529  onpwsuc  7531  onpsssuc  7534  onsucmin  7536  ordunpr  7541  ordunisuc  7547  onsucuni2  7549  onuninsuci  7555  ordunisuc2  7559  ordzsl  7560  onzsl  7561  nlimon  7566  tfinds  7574  tfindsg2  7576  nnord  7588  onfununi  7978  smo11  8001  smoord  8002  smoword  8003  smogt  8004  tfrlem1  8012  tfrlem9a  8022  tfrlem15  8028  tz7.44-2  8043  tz7.48lem  8077  oe0m1  8146  oaordi  8172  oaord  8173  oacan  8174  oawordri  8176  oalimcl  8186  oaass  8187  omord2  8193  omcan  8195  omwordi  8197  omword1  8199  omword2  8200  om00  8201  omlimcl  8204  omass  8206  omeulem2  8209  omopth2  8210  oen0  8212  oeord  8214  oecan  8215  oewordi  8217  oeworde  8219  oelimcl  8226  oeeulem  8227  oeeui  8228  nnarcl  8242  nnawordi  8247  nnawordex  8263  oaabs2  8272  omabs  8274  omsmo  8281  omxpenlem  8618  infensuc  8695  onomeneq  8708  ordiso  8980  ordtypelem2  8983  hartogslem1  9006  cantnflt  9135  cantnfp1lem3  9143  cantnfp1  9144  oemapso  9145  oemapvali  9147  cantnflem1d  9151  cantnflem1  9152  cantnf  9156  oemapwe  9157  cantnffval2  9158  cnfcom  9163  r111  9204  r1ordg  9207  rankonidlem  9257  bndrank  9270  r1pw  9274  r1pwALT  9275  rankbnd2  9298  tcrank  9313  cardprclem  9408  carduni  9410  cardmin2  9427  infxpenlem  9439  alephdom  9507  alephdom2  9513  cardaleph  9515  iscard3  9519  alephfp  9534  dfac12lem1  9569  dfac12lem2  9570  dfac12lem3  9571  cflim2  9685  cofsmo  9691  cfsmolem  9692  coftr  9695  cfcof  9696  fin67  9817  hsmexlem5  9852  zorn2lem6  9923  ttukeylem3  9933  ttukeylem5  9935  ttukeylem6  9936  ttukeylem7  9937  winainflem  10115  r1limwun  10158  r1wunlim  10159  tsksuc  10184  inar1  10197  gruina  10240  grur1a  10241  grur1  10242  dfrdg2  33040  poseq  33095  soseq  33096  nodmord  33160  noextendseq  33174  noextenddif  33175  nosupno  33203  nosupres  33207  noetalem3  33219  ontgval  33779  ontgsucval  33780  onsuctopon  33782  onintopssconn  33788  onsuct0  33789  sucneqond  34649  onsucuni3  34651  aomclem4  39677  aomclem5  39678  dfsucon  39909  nndomog  39917  onfrALTlem3  40898  onfrALTlem2  40900  onfrALTlem3VD  41241  onfrALTlem2VD  41243  onsetreclem3  44829