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

Theorem elong 6392
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 6391 . 2 (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴))
2 df-on 6388 . 2 On = {𝑥 ∣ Ord 𝑥}
31, 2elab2g 3680 1 (𝐴𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wcel 2108  Ord word 6383  Oncon0 6384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-ss 3968  df-uni 4908  df-tr 5260  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388
This theorem is referenced by:  elon  6393  eloni  6394  elon2  6395  ordelon  6408  onin  6415  limelon  6448  ordsssuc2  6475  onprc  7798  ssonuni  7800  sucexeloni  7829  sucexeloniOLD  7830  suceloniOLD  7832  ordsucOLD  7834  cofon1  8710  cofon2  8711  enp1i  9313  oion  9576  hartogs  9584  card2on  9594  tskwe  9990  onssnum  10080  hsmexlem1  10466  ondomon  10603  1stcrestlem  23460  nosupno  27748  noinfno  27763  hfninf  36187  rn1st  45280
  Copyright terms: Public domain W3C validator