Theorem eloni 5875

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

Syntax hints:   → wi 4   ∈ wcel 2145  Ord word 5864  Oncon0 5865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-v 3353  df-in 3730  df-ss 3737  df-uni 4576  df-tr 4888  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-ord 5868  df-on 5869

This theorem is referenced by:  onelon  5890  onin  5896  ontri1  5899  onfr  5905  onelpss  5906  onsseleq  5907  onelss  5908  ontr1  5913  ontr2  5914  ordunidif  5915  on0eln0  5922  ordsssuc  5954  onsssuc  5955  onnbtwn  5960  suc11  5973  onordi  5974  onssneli  5979  ordon  7133  ordeleqon  7139  onss  7141  ordsuc  7165  onpwsuc  7167  onpsssuc  7170  onsucmin  7172  ordunpr  7177  ordunisuc  7183  onsucuni2  7185  onuninsuci  7191  ordunisuc2  7195  ordzsl  7196  onzsl  7197  nlimon  7202  tfinds  7210  tfindsg2  7212  nnord  7224  onfununi  7595  smo11  7618  smoord  7619  smoword  7620  smogt  7621  tfrlem1  7629  tfrlem9a  7639  tfrlem15  7645  tz7.44-2  7660  tz7.48lem  7693  oe0m1  7759  oaordi  7784  oaord  7785  oacan  7786  oawordri  7788  oalimcl  7798  oaass  7799  omord2  7805  omcan  7807  omwordi  7809  omword1  7811  omword2  7812  om00  7813  omlimcl  7816  omass  7818  omeulem2  7821  omopth2  7822  oen0  7824  oeord  7826  oecan  7827  oewordi  7829  oeworde  7831  oelimcl  7838  oeeulem  7839  oeeui  7840  nnarcl  7854  nnawordi  7859  nnawordex  7875  oaabs2  7883  omabs  7885  omsmo  7892  omxpenlem  8221  infensuc  8298  onomeneq  8310  ordiso  8581  ordtypelem2  8584  hartogslem1  8607  cantnflt  8737  cantnfp1lem3  8745  cantnfp1  8746  oemapso  8747  oemapvali  8749  cantnflem1d  8753  cantnflem1  8754  cantnf  8758  oemapwe  8759  cantnffval2  8760  cnfcom  8765  r111  8806  r1ordg  8809  rankonidlem  8859  bndrank  8872  r1pw  8876  r1pwALT  8877  rankbnd2  8900  tcrank  8915  cardprclem  9009  carduni  9011  cardmin2  9028  infxpenlem  9040  alephdom  9108  alephdom2  9114  cardaleph  9116  iscard3  9120  alephfp  9135  dfac12lem1  9171  dfac12lem2  9172  dfac12lem3  9173  cflim2  9291  cofsmo  9297  cfsmolem  9298  coftr  9301  cfcof  9302  fin67  9423  hsmexlem5  9458  zorn2lem6  9529  ttukeylem3  9539  ttukeylem5  9541  ttukeylem6  9542  ttukeylem7  9543  winainflem  9721  r1limwun  9764  r1wunlim  9765  tsksuc  9790  inar1  9803  gruina  9846  grur1a  9847  grur1  9848  dfrdg2  32037  poseq  32090  soseq  32091  nodmord  32143  noextendseq  32157  noextenddif  32158  nosupno  32186  nosupres  32190  noetalem3  32202  ontgval  32767  ontgsucval  32768  onsuctopon  32770  onintopssconn  32776  onsuct0  32777  sucneqond  33549  onsucuni3  33551  aomclem4  38151  aomclem5  38152  onfrALTlem3  39282  onfrALTlem2  39284  onfrALTlem3VD  39643  onfrALTlem2VD  39645  onsetreclem3  42976