Theorem el1o 7168

Description: Membership in ordinal one. (Contributed by NM, 5-Jan-2005.)

Assertion

Ref	Expression
el1o

Proof of Theorem el1o

Step	Hyp	Ref	Expression
1		df1o2 7161	. . 3
2	1	eleq2i 2535	. 2
3		0ex 4582	. . 3
4	3	elsnc2 4060	. 2
5	2, 4	bitri 249	1

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