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

Theorem el1o 7168
 Description: Membership in ordinal one. (Contributed by NM, 5-Jan-2005.)
Assertion
Ref Expression
el1o

Proof of Theorem el1o
StepHypRef Expression
1 df1o2 7161 . . 3
21eleq2i 2535 . 2
3 0ex 4582 . . 3
43elsnc2 4060 . 2
52, 4bitri 249 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  =wceq 1395  e.wcel 1818   c0 3784  {csn 4029   c1o 7142 This theorem is referenced by:  0lt1o  7173  oelim2  7263  oeeulem  7269  oaabs2  7313  map0e  7476  map1  7614  cantnff  8114  cnfcom3lem  8168  cnfcom3lemOLD  8176  cfsuc  8658  pf1ind  18391  mavmul0  19054  cramer0  19192 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-nul 4581 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-un 3480  df-nul 3785  df-sn 4030  df-suc 4889  df-1o 7149
 Copyright terms: Public domain W3C validator