Theorem df1o2 4133

Description: Expanded value of the ordinal number 1.

Assertion

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

Proof of Theorem df1o2

Step	Hyp	Ref	Expression
1		df-1o 4126	. 2 |- 1o = suc (/)
2		suc0 3039	. 2 |- suc (/) = {(/)}
3	1, 2	eqtr 1493	1 |- 1o = {(/)}

Syntax hints:   = wceq 955  (/)c0 2277  {csn 2406  suc csuc 2946  1oc1o 4121

This theorem is referenced by:  df2o2 4134  1ne0 4135  el1o 4139  map0e 4335  map0 4337  ensn1 4414  en1 4416  map1 4420  1sdom2 4514  pwfi 4554  xp1en 4910  xp2cda 4911  infmap2 7541

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-dif 2046  df-un 2047  df-nul 2278  df-suc 2950  df-1o 4126

Copyright terms: Public domain