Theorem df2o3 8470

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 8463	. 2 ⊢ 2o = suc 1o
2		df-suc 6367	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8469	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4158	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4630	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2763	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2764	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1541   ∪ cun 3945  ∅c0 4321  {csn 4627  {cpr 4629  suc csuc 6363  1_oc1o 8455  2_oc2o 8456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-un 3952  df-nul 4322  df-pr 4630  df-suc 6367  df-1o 8462  df-2o 8463

This theorem is referenced by:  df2o2  8471  2oex  8473  nlim2  8486  ord2eln012  8493  2oconcl  8499  enpr2d  9045  map2xp  9143  snnen2o  9233  rex2dom  9242  1sdom2dom  9243  1sdomOLD  9245  cantnflem2  9681  xp2dju  10167  sdom2en01  10293  sadcf  16390  fnpr2o  17499  fnpr2ob  17500  fvprif  17503  xpsfrnel  17504  xpsfeq  17505  xpsle  17521  setcepi  18034  setc2obas  18040  setc2ohom  18041  efgi0  19582  efgi1  19583  vrgpf  19630  vrgpinv  19631  frgpuptinv  19633  frgpup2  19638  frgpup3lem  19639  frgpnabllem1  19735  dmdprdpr  19913  dprdpr  19914  xpstopnlem1  23304  xpstopnlem2  23306  xpsxmetlem  23876  xpsdsval  23878  xpsmet  23879  onint1  35322  pw2f1ocnv  41761  wepwsolem  41769  omnord1ex  42039  oege2  42042  df3o2  42048  oenord1ex  42050  oenord1  42051  oaomoencom  42052  oenassex  42053  omabs2  42067  omcl3g  42069  clsk1independent  42782