Theorem df1o2 6522

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 6509	. 2 ⊢ 1o = suc ∅
2		suc0 4462	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2227	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1373  ∅c0 3461  {csn 3634  suc csuc 4416  1_oc1o 6502

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-dif 3169  df-un 3171  df-nul 3462  df-suc 4422  df-1o 6509

This theorem is referenced by:  df2o3  6523  df2o2  6524  1n0  6525  el1o  6530  dif1o  6531  ensn1  6895  en1  6898  map1  6911  xp1en  6925  exmidpw  7012  exmidpweq  7013  pw1fin  7014  pw1dc0el  7015  exmidpw2en  7016  ss1o0el1o  7017  unfiexmid  7022  0ct  7216  exmidonfinlem  7308  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  pw1on  7345  pw1dom2  7346  pw1ne1  7348  sucpw1nel3  7352  fihashen1  10951  ss1oel2o  16002  pwle2  16009  pwf1oexmid  16010  sbthom  16039