Theorem eloni 6203

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ord word 6192  Oncon0 6193

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841  df-tr 5175  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-ord 6196  df-on 6197

This theorem is referenced by:  onelon  6218  onin  6224  ontri1  6227  onfr  6232  onelpss  6233  onsseleq  6234  onelss  6235  ontr1  6239  ontr2  6240  ordunidif  6241  on0eln0  6248  ordsssuc  6279  onsssuc  6280  onnbtwn  6284  suc11  6296  onordi  6297  onssneli  6302  epweon  7499  ordeleqon  7505  onss  7507  ordsuc  7531  onpwsuc  7533  onpsssuc  7536  onsucmin  7538  ordunpr  7543  ordunisuc  7549  onsucuni2  7551  onuninsuci  7557  ordunisuc2  7561  ordzsl  7562  onzsl  7563  nlimon  7568  tfinds  7576  tfindsg2  7578  nnord  7590  onfununi  7980  smo11  8003  smoord  8004  smoword  8005  smogt  8006  tfrlem1  8014  tfrlem9a  8024  tfrlem15  8030  tz7.44-2  8045  tz7.48lem  8079  oe0m1  8148  oaordi  8174  oaord  8175  oacan  8176  oawordri  8178  oalimcl  8188  oaass  8189  omord2  8195  omcan  8197  omwordi  8199  omword1  8201  omword2  8202  om00  8203  omlimcl  8206  omass  8208  omeulem2  8211  omopth2  8212  oen0  8214  oeord  8216  oecan  8217  oewordi  8219  oeworde  8221  oelimcl  8228  oeeulem  8229  oeeui  8230  nnarcl  8244  nnawordi  8249  nnawordex  8265  oaabs2  8274  omabs  8276  omsmo  8283  omxpenlem  8620  infensuc  8697  onomeneq  8710  ordiso  8982  ordtypelem2  8985  hartogslem1  9008  cantnflt  9137  cantnfp1lem3  9145  cantnfp1  9146  oemapso  9147  oemapvali  9149  cantnflem1d  9153  cantnflem1  9154  cantnf  9158  oemapwe  9159  cantnffval2  9160  cnfcom  9165  r111  9206  r1ordg  9209  rankonidlem  9259  bndrank  9272  r1pw  9276  r1pwALT  9277  rankbnd2  9300  tcrank  9315  cardprclem  9410  carduni  9412  cardmin2  9429  infxpenlem  9441  alephdom  9509  alephdom2  9515  cardaleph  9517  iscard3  9521  alephfp  9536  dfac12lem1  9571  dfac12lem2  9572  dfac12lem3  9573  cflim2  9687  cofsmo  9693  cfsmolem  9694  coftr  9697  cfcof  9698  fin67  9819  hsmexlem5  9854  zorn2lem6  9925  ttukeylem3  9935  ttukeylem5  9937  ttukeylem6  9938  ttukeylem7  9939  winainflem  10117  r1limwun  10160  r1wunlim  10161  tsksuc  10186  inar1  10199  gruina  10242  grur1a  10243  grur1  10244  dfrdg2  33042  poseq  33097  soseq  33098  nodmord  33162  noextendseq  33176  noextenddif  33177  nosupno  33205  nosupres  33209  noetalem3  33221  ontgval  33781  ontgsucval  33782  onsuctopon  33784  onintopssconn  33790  onsuct0  33791  sucneqond  34648  onsucuni3  34650  aomclem4  39664  aomclem5  39665  dfsucon  39896  nndomog  39904  onfrALTlem3  40885  onfrALTlem2  40887  onfrALTlem3VD  41228  onfrALTlem2VD  41230  onsetreclem3  44816