Theorem df2o3 8282

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 8268	. 2 ⊢ 2o = suc 1o
2		df-suc 6257	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8279	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4089	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4561	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2769	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2770	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1539   ∪ cun 3881  ∅c0 4253  {csn 4558  {cpr 4560  suc csuc 6253  1_oc1o 8260  2_oc2o 8261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-pr 4561  df-suc 6257  df-1o 8267  df-2o 8268

This theorem is referenced by:  df2o2  8283  2oex  8284  2oconcl  8295  map2xp  8883  1sdom  8955  cantnflem2  9378  xp2dju  9863  sdom2en01  9989  sadcf  16088  fnpr2o  17185  fnpr2ob  17186  fvprif  17189  xpsfrnel  17190  xpsfeq  17191  xpsle  17207  setcepi  17719  setc2obas  17725  setc2ohom  17726  efgi0  19241  efgi1  19242  vrgpf  19289  vrgpinv  19290  frgpuptinv  19292  frgpup2  19297  frgpup3lem  19298  frgpnabllem1  19389  dmdprdpr  19567  dprdpr  19568  xpstopnlem1  22868  xpstopnlem2  22870  xpsxmetlem  23440  xpsdsval  23442  xpsmet  23443  onint1  34565  pw2f1ocnv  40775  wepwsolem  40783  df3o2  41523  clsk1independent  41545