Theorem eloni 4387

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

Syntax hints:   → wi 4   ∈ wcel 2158  Ord word 4374  Oncon0 4375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-v 2751  df-in 3147  df-ss 3154  df-uni 3822  df-tr 4114  df-iord 4378  df-on 4380

This theorem is referenced by:  elon2  4388  onelon  4396  onin  4398  onelss  4399  ontr1  4401  onordi  4438  onss  4504  onsuc  4512  onsucb  4514  onsucmin  4518  onsucelsucr  4519  onintonm  4528  ordsucunielexmid  4542  onsucuni2  4575  nnord  4623  tfrlem1  6323  tfrlemisucaccv  6340  tfrlemibfn  6343  tfrlemiubacc  6345  tfrexlem  6349  tfr1onlemsucfn  6355  tfr1onlemsucaccv  6356  tfr1onlembfn  6359  tfr1onlemubacc  6361  tfrcllemsucfn  6368  tfrcllemsucaccv  6369  tfrcllembfn  6372  tfrcllemubacc  6374  sucinc2  6461  phplem4on  6881  ordiso  7049