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

Theorem elong 5648
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 5647 . 2 (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴))
2 df-on 5644 . 2 On = {𝑥 ∣ Ord 𝑥}
31, 2elab2g 3322 1 (𝐴𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wcel 1977  Ord word 5639  Oncon0 5640
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-uni 4373  df-tr 4681  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-on 5644
This theorem is referenced by:  elon  5649  eloni  5650  elon2  5651  ordelon  5664  onin  5671  limelon  5705  ordsssuc2  5731  onprc  6876  ssonuni  6878  suceloni  6905  ordsuc  6906  oion  8324  hartogs  8332  card2on  8342  tskwe  8659  onssnum  8746  hsmexlem1  9131  ondomon  9264  1stcrestlem  21065  hfninf  31463
  Copyright terms: Public domain W3C validator