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

Theorem el1o 8438
Description: Membership in ordinal one. (Contributed by NM, 5-Jan-2005.)
Assertion
Ref Expression
el1o (𝐴 ∈ 1o𝐴 = ∅)

Proof of Theorem el1o
StepHypRef Expression
1 df1o2 8416 . . 3 1o = {∅}
21eleq2i 2829 . 2 (𝐴 ∈ 1o𝐴 ∈ {∅})
3 0ex 5263 . . 3 ∅ ∈ V
43elsn2 4624 . 2 (𝐴 ∈ {∅} ↔ 𝐴 = ∅)
52, 4bitri 274 1 (𝐴 ∈ 1o𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1541  wcel 2106  c0 4281  {csn 4585  1oc1o 8402
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-nul 5262
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3446  df-dif 3912  df-un 3914  df-nul 4282  df-sn 4586  df-suc 6322  df-1o 8409
This theorem is referenced by:  ord1eln01  8439  ord2eln012  8440  0lt1o  8447  oelim2  8539  oeeulem  8545  oaabs2  8592  cantnff  9607  cnfcom3lem  9636  cfsuc  10190  pf1ind  21717  mavmul0  21897  cramer0  22035  cantnfresb  41634  omabs2  41641  omcl3g  41643  f1omo  46897
  Copyright terms: Public domain W3C validator