Theorem eloni 4496

Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
eloni	|- ( A e. On -> Ord A )

Proof of Theorem eloni

Step	Hyp	Ref	Expression
1		elong 4494	. 2 |- ( A e. On -> ( A e. On <-> Ord A ) )
2	1	ibi 176	1 |- ( A e. On -> Ord A )

Syntax hints:   -> wi 4   e. wcel 2203   Ord word 4483   Oncon0 4484

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-in 3217  df-ss 3224  df-uni 3915  df-tr 4209  df-iord 4487  df-on 4489

This theorem is referenced by:  elon2  4497  onelon  4505  onin  4507  onelss  4508  ontr1  4510  onordi  4547  onss  4615  onsuc  4623  onsucb  4625  onsucmin  4629  onsucelsucr  4630  onintonm  4639  ordsucunielexmid  4653  onsucuni2  4686  nnord  4734  tfrlem1  6539  tfrlemisucaccv  6556  tfrlemibfn  6559  tfrlemiubacc  6561  tfrexlem  6565  tfr1onlemsucfn  6571  tfr1onlemsucaccv  6572  tfr1onlembfn  6575  tfr1onlemubacc  6577  tfrcllemsucfn  6584  tfrcllemsucaccv  6585  tfrcllembfn  6588  tfrcllemubacc  6590  sucinc2  6679  phplem4on  7122  ordiso  7327