HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem eloni 2948
Description: An ordinal number has the ordinal property.
Assertion
Ref Expression
eloni |- (A e. On -> Ord A)
Proof of Theorem eloni
StepHypRef Expression
1 elong 2946 . 2 |- (A e. On -> (A e. On <-> Ord A))
21ibi 590 1 |- (A e. On -> Ord A)
Colors of variables: wff set class
Syntax hints:   -> wi 3   e. wcel 955  Ord word 2937  Oncon0 2938
This theorem is referenced by:  elon2 2949  onelon 2962  onin 2968  ontri1 2971  ordon 2977  ordeleqon 2980  onsst 2982  ssorduni 2983  onelpsst 2988  onsseleq 2989  onelsst 2990  ontr1 2993  ontr2 2994  ordunidif 2995  on0eln0 3014  ordsssuc 3047  onsssuc 3048  onnbtwn 3054  ordsuc 3055  onpwsuc 3057  onsucmin 3062  ordunisuc 3079  onsucuni2 3081  suc11 3083  onord 3085  onssneli 3091  onuninsuc 3098  ordunisuc2 3105  ordzsl 3106  nlimon 3112  nnord 3130  tfinds 3151  tfindsg2 3153  tz7.48lem 3940  oe0m1 4144  oesuc 4150  oaordi 4164  oaord 4165  oacan 4166  oawordri 4168  oalimcl 4178  oaass 4179  omord2 4182  omcan 4184  omwordi 4186  omword1 4188  omword2 4189  om00 4190  omlimcl 4193  omass 4195  oen0 4197  oeord 4199  oecan 4200  oewordi 4202  oeworde 4204  nnarcl 4216  oaabs 4236  omsmo 4241  onomeneq 4498  infensuc 4610  r1ord 4627  r1val1 4630  rankr1 4646  rankval3 4653  bndrank 4654  r1pw 4658  rankbnd2 4676  weth 4759  zorn2lem6 4765  cardnn 4796  ondomcard 4829  carduni 4830  cardaleph 4857  iscard3 4860  alephfp 4872
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-ral 1641  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-tr 2671  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942
Copyright terms: Public domain