Theorem eloni 4472

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

Syntax hints:   → wi 4   ∈ wcel 2202  Ord word 4459  Oncon0 4460

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-in 3206  df-ss 3213  df-uni 3894  df-tr 4188  df-iord 4463  df-on 4465

This theorem is referenced by:  elon2  4473  onelon  4481  onin  4483  onelss  4484  ontr1  4486  onordi  4523  onss  4591  onsuc  4599  onsucb  4601  onsucmin  4605  onsucelsucr  4606  onintonm  4615  ordsucunielexmid  4629  onsucuni2  4662  nnord  4710  tfrlem1  6474  tfrlemisucaccv  6491  tfrlemibfn  6494  tfrlemiubacc  6496  tfrexlem  6500  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembfn  6510  tfr1onlemubacc  6512  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembfn  6523  tfrcllemubacc  6525  sucinc2  6614  phplem4on  7054  ordiso  7235