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

Theorem elong 6171
 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 variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordeq 6170 . 2 (𝑦 = 𝑥 → (Ord 𝑦 ↔ Ord 𝑥))
2 ordeq 6170 . 2 (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴))
3 df-on 6167 . 2 On = {𝑦 ∣ Ord 𝑦}
41, 2, 3elab2gw 3616 1 (𝐴𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2112  Ord word 6162  Oncon0 6163 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-v 3446  df-in 3891  df-ss 3901  df-uni 4804  df-tr 5140  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-ord 6166  df-on 6167 This theorem is referenced by:  elon  6172  eloni  6173  elon2  6174  ordelon  6187  onin  6194  limelon  6226  ordsssuc2  6251  onprc  7483  ssonuni  7485  suceloni  7512  ordsuc  7513  oion  8988  hartogs  8996  card2on  9006  tskwe  9367  onssnum  9455  hsmexlem1  9841  ondomon  9978  1stcrestlem  22060  nosupno  33311  hfninf  33755
 Copyright terms: Public domain W3C validator