Theorem df1o2 6660

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 6646	. 2 |- 1o = suc (/)
2		suc0 4531	. 2 |- suc (/) = { (/) }
3	1, 2	eqtri 2253	1 |- 1o = { (/) }

Syntax hints:   = wceq 1398   (/)c0 3507   {csn 3688   suc csuc 4485   1oc1o 6639

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-dif 3212  df-un 3214  df-nul 3508  df-suc 4491  df-1o 6646

This theorem is referenced by:  df2o3  6661  df2o2  6662  1n0  6664  el1o  6669  dif1o  6670  ensn1  7035  en1  7038  map1  7053  dom1o  7068  xp1en  7073  exmidpw  7167  exmidpweq  7168  pw1fin  7169  pw1dc0el  7170  exmidpw2en  7171  ss1o0el1o  7172  unfiexmid  7177  0ct  7397  exmidonfinlem  7495  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  pw1m  7533  pw1on  7535  pw1dom2  7536  pw1ne1  7538  sucpw1nel3  7542  fihashen1  11157  ss1oel2o  16748  pw1ndom3lem  16750  pwle2  16759  pwf1oexmid  16760  exmidnotnotr  16766  sbthom  16793