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

Theorem elong 6379
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 6378 . 2 (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴))
2 df-on 6375 . 2 On = {𝑥 ∣ Ord 𝑥}
31, 2elab2g 3666 1 (𝐴𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2098  Ord word 6370  Oncon0 6371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-v 3463  df-ss 3961  df-uni 4910  df-tr 5267  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-ord 6374  df-on 6375
This theorem is referenced by:  elon  6380  eloni  6381  elon2  6382  ordelon  6395  onin  6402  limelon  6435  ordsssuc2  6462  onprc  7781  ssonuni  7783  sucexeloni  7813  sucexeloniOLD  7814  suceloniOLD  7816  ordsucOLD  7818  cofon1  8693  cofon2  8694  enp1i  9304  oion  9561  hartogs  9569  card2on  9579  tskwe  9975  onssnum  10065  hsmexlem1  10451  ondomon  10588  1stcrestlem  23400  nosupno  27682  noinfno  27697  hfninf  35913  rn1st  44788
  Copyright terms: Public domain W3C validator