Theorem eloni 4406

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

Syntax hints:   → wi 4   ∈ wcel 2164  Ord word 4393  Oncon0 4394

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-in 3159  df-ss 3166  df-uni 3836  df-tr 4128  df-iord 4397  df-on 4399

This theorem is referenced by:  elon2  4407  onelon  4415  onin  4417  onelss  4418  ontr1  4420  onordi  4457  onss  4525  onsuc  4533  onsucb  4535  onsucmin  4539  onsucelsucr  4540  onintonm  4549  ordsucunielexmid  4563  onsucuni2  4596  nnord  4644  tfrlem1  6361  tfrlemisucaccv  6378  tfrlemibfn  6381  tfrlemiubacc  6383  tfrexlem  6387  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembfn  6397  tfr1onlemubacc  6399  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembfn  6410  tfrcllemubacc  6412  sucinc2  6499  phplem4on  6923  ordiso  7095