Theorem df2o3 8467

Description: Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.)

Assertion

Ref	Expression
df2o3	⊢ 2o = {∅, 1o}

Proof of Theorem df2o3

Step	Hyp	Ref	Expression
1		df-2o 8460	. 2 ⊢ 2o = suc 1o
2		df-suc 6370	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8466	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4118	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4594	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2791	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2792	1 ⊢ 2o = {∅, 1o}

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3904  ∅c0 4286  {csn 4591  {cpr 4593  suc csuc 6366  1_oc1o 8452  2_oc2o 8453

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-un 3911  df-nul 4287  df-pr 4594  df-suc 6370  df-1o 8459  df-2o 8460

This theorem is used by:  df2o2  8468  2oex  8471  nlim2  8481  ord2eln012  8488  2oconcl  8494  enpr2d  9052  map2xp  9142  snnen2o  9212  rex2dom  9220  1sdom2dom  9221  cantnflem2  9666  xp2dju  10176  sdom2en01  10301  sadcf  16535  fnpr2o  17635  fnpr2ob  17636  fvprif  17639  xpsfrnel  17640  xpsfeq  17641  xpsle  17657  setcepi  18169  setc2obas  18175  setc2ohom  18176  efgi0  19836  efgi1  19837  vrgpf  19884  vrgpinv  19885  frgpuptinv  19887  frgpup2  19892  frgpup3lem  19893  frgpnabllem1  19989  dmdprdpr  20167  dprdpr  20168  xpstopnlem1  24019  xpstopnlem2  24021  xpsxmetlem  24589  xpsdsval  24591  xpsmet  24592  bdaypw2n0bndlem  28709  onint1  37019  pw2f1ocnv  43824  wepwsolem  43829  omnord1ex  44091  oege2  44094  df3o2  44100  oenord1ex  44102  oenord1  44103  oaomoencom  44104  oenassex  44105  omabs2  44119  omcl3g  44121  clsk1independent  44832  setc1onsubc  50439