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

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

Proof of Theorem el1o
StepHypRef Expression
1 df1o2 8513 . . 3 1o = {∅}
21eleq2i 2833 . 2 (𝐴 ∈ 1o𝐴 ∈ {∅})
3 0ex 5307 . . 3 ∅ ∈ V
43elsn2 4665 . 2 (𝐴 ∈ {∅} ↔ 𝐴 = ∅)
52, 4bitri 275 1 (𝐴 ∈ 1o𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  wcel 2108  c0 4333  {csn 4626  1oc1o 8499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334  df-sn 4627  df-suc 6390  df-1o 8506
This theorem is referenced by:  ord1eln01  8534  ord2eln012  8535  0lt1o  8542  oelim2  8633  oeeulem  8639  oaabs2  8687  cantnff  9714  cnfcom3lem  9743  cfsuc  10297  pf1ind  22359  mavmul0  22558  cramer0  22696  cantnfresb  43337  omabs2  43345  omcl3g  43347  f1omo  48792
  Copyright terms: Public domain W3C validator