MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elong Structured version   Visualization version   GIF version

Theorem elong 6323
Description: An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
elong (𝐴𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))

Proof of Theorem elong
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ordeq 6322 . 2 (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴))
2 df-on 6319 . 2 On = {𝑥 ∣ Ord 𝑥}
31, 2elab2g 3630 1 (𝐴𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2106  Ord word 6314  Oncon0 6315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-v 3445  df-in 3915  df-ss 3925  df-uni 4864  df-tr 5221  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-ord 6318  df-on 6319
This theorem is referenced by:  elon  6324  eloni  6325  elon2  6326  ordelon  6339  onin  6346  limelon  6379  ordsssuc2  6406  onprc  7708  ssonuni  7710  sucexeloni  7740  sucexeloniOLD  7741  suceloniOLD  7743  ordsucOLD  7745  cofon1  8614  cofon2  8615  enp1i  9219  oion  9468  hartogs  9476  card2on  9486  tskwe  9882  onssnum  9972  hsmexlem1  10358  ondomon  10495  1stcrestlem  22787  nosupno  27035  noinfno  27050  hfninf  34738  rn1st  43439
  Copyright terms: Public domain W3C validator