Theorem eloni 2209

Description: An ordinal number has the ordinal property.

Assertion

Ref	Expression
eloni	⊢ (A ∈ On → Ord A)

Proof of Theorem eloni

Step	Hyp	Ref	Expression
1		elong 2207	. 2 ⊢ (A ∈ On → (A ∈ On ↔ Ord A))
2	1	ibi 449	1 ⊢ (A ∈ On → Ord A)

Syntax hints:   → wi 2   ∈ wcel 1092  Ord word 2198  Oncon0 2199

This theorem is referenced by:  elon2 2210  onelon 2223  onin 2229  ontri1 2232  ordon 2238  ordeleqon 2241  onsst 2243  ssorduni 2249  onelpsst 2253  onsseleq 2254  onelsst 2255  ontr1 2258  ontr2 2259  ordunidif 2260  on0eln0 2279  ordsssuc 2310  onsssuc 2311  onnbtwn 2317  ordsuc 2318  onsucmin 2323  ordunisuc 2339  suc11 2341  onord 2343  onssneli 2349  onuninsuc 2356  ordzsl 2366  nlimon 2369  nnord 2381  tfinds 2401  tfindsg2 2403  tfrlem10 2958  tz7.48lem 2993  oesuc 3134  oaordi 3148  oaord 3149  oacan 3150  oawordri 3152  oalimcl 3162  oaass 3163  oen0 3165  nnarcl 3174  omsmo 3196  onomeneq 3414  infensuc 3484  r1ord 3499  r1val1 3502  rankr1 3518  r1val2 3522  rankval3 3525  bndrank 3526  r1pw 3529  weth 3602  zornlem6 3608  cardnn 3631  ondomcard 3663  carduni 3664  cardaleph 3690  iscard3 3693

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203

metamath.org