Theorem df1o2 6601

Description: Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)

Assertion

Ref	Expression
df1o2	|- 1o = { (/) }

Proof of Theorem df1o2

Step	Hyp	Ref	Expression
1		df-1o 6587	. 2 |- 1o = suc (/)
2		suc0 4510	. 2 |- suc (/) = { (/) }
3	1, 2	eqtri 2251	1 |- 1o = { (/) }

Syntax hints:   = wceq 1397   (/)c0 3493   {csn 3670   suc csuc 4464   1oc1o 6580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-dif 3201  df-un 3203  df-nul 3494  df-suc 4470  df-1o 6587

This theorem is referenced by:  df2o3  6602  df2o2  6603  1n0  6605  el1o  6610  dif1o  6611  ensn1  6975  en1  6978  map1  6992  dom1o  7007  xp1en  7012  exmidpw  7105  exmidpweq  7106  pw1fin  7107  pw1dc0el  7108  exmidpw2en  7109  ss1o0el1o  7110  unfiexmid  7115  0ct  7311  exmidonfinlem  7409  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  pw1m  7447  pw1on  7449  pw1dom2  7450  pw1ne1  7452  sucpw1nel3  7456  fihashen1  11067  ss1oel2o  16646  pw1ndom3lem  16648  pwle2  16659  pwf1oexmid  16660  exmidnotnotr  16666  sbthom  16693