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

Theorem elong 6079
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 6078 . 2 (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴))
2 df-on 6075 . 2 On = {𝑥 ∣ Ord 𝑥}
31, 2elab2g 3608 1 (𝐴𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wcel 2081  Ord word 6070  Oncon0 6071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-in 3870  df-ss 3878  df-uni 4750  df-tr 5069  df-po 5367  df-so 5368  df-fr 5407  df-we 5409  df-ord 6074  df-on 6075
This theorem is referenced by:  elon  6080  eloni  6081  elon2  6082  ordelon  6095  onin  6102  limelon  6134  ordsssuc2  6159  onprc  7360  ssonuni  7362  suceloni  7389  ordsuc  7390  oion  8851  hartogs  8859  card2on  8869  tskwe  9230  onssnum  9317  hsmexlem1  9699  ondomon  9836  1stcrestlem  21749  nosupno  32818  hfninf  33262
  Copyright terms: Public domain W3C validator