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

Theorem elon 6364
Description: An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
Hypothesis
Ref Expression
elon.1 𝐴 ∈ V
Assertion
Ref Expression
elon (𝐴 ∈ On ↔ Ord 𝐴)

Proof of Theorem elon
StepHypRef Expression
1 elon.1 . 2 𝐴 ∈ V
2 elong 6363 . 2 (𝐴 ∈ V → (𝐴 ∈ On ↔ Ord 𝐴))
31, 2ax-mp 5 1 (𝐴 ∈ On ↔ Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wcel 2098  Vcvv 3466  Ord word 6354  Oncon0 6355
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 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-v 3468  df-in 3948  df-ss 3958  df-uni 4901  df-tr 5257  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-ord 6358  df-on 6359
This theorem is referenced by:  tron  6378  0elon  6409  smogt  8363  dfrecs3  8368  dfrecs3OLD  8369  rdglim2  8428  omeulem1  8578  naddcllem  8672  isfinite2  9298  r0weon  10004  cflim3  10254  inar1  10767  addsproplem7  27811  ellimits  35378  dford3lem2  42280
  Copyright terms: Public domain W3C validator