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

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

Proof of Theorem el1o
StepHypRef Expression
1 df1o2 8423 . . 3 1o = {∅}
21eleq2i 2826 . 2 (𝐴 ∈ 1o𝐴 ∈ {∅})
3 0ex 5268 . . 3 ∅ ∈ V
43elsn2 4629 . 2 (𝐴 ∈ {∅} ↔ 𝐴 = ∅)
52, 4bitri 275 1 (𝐴 ∈ 1o𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  wcel 2107  c0 4286  {csn 4590  1oc1o 8409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5267
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3449  df-dif 3917  df-un 3919  df-nul 4287  df-sn 4591  df-suc 6327  df-1o 8416
This theorem is referenced by:  ord1eln01  8446  ord2eln012  8447  0lt1o  8454  oelim2  8546  oeeulem  8552  oaabs2  8599  cantnff  9618  cnfcom3lem  9647  cfsuc  10201  pf1ind  21744  mavmul0  21924  cramer0  22062  cantnfresb  41706  omabs2  41714  omcl3g  41716  f1omo  47017
  Copyright terms: Public domain W3C validator