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

Theorem elon 6372
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 6371 . 2 (𝐴 ∈ V → (𝐴 ∈ On ↔ Ord 𝐴))
31, 2ax-mp 5 1 (𝐴 ∈ On ↔ Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wcel 2099  Vcvv 3470  Ord word 6362  Oncon0 6363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3058  df-v 3472  df-in 3952  df-ss 3962  df-uni 4904  df-tr 5260  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-ord 6366  df-on 6367
This theorem is referenced by:  tron  6386  0elon  6417  smogt  8381  dfrecs3  8386  dfrecs3OLD  8387  rdglim2  8446  omeulem1  8596  naddcllem  8690  isfinite2  9319  r0weon  10029  cflim3  10279  inar1  10792  addsproplem7  27885  ellimits  35500  dford3lem2  42442
  Copyright terms: Public domain W3C validator