Theorem df2o3 8393

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 8386	. 2 ⊢ 2o = suc 1o
2		df-suc 6312	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8392	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4111	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4576	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2757	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2758	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1541   ∪ cun 3895  ∅c0 4280  {csn 4573  {cpr 4575  suc csuc 6308  1_oc1o 8378  2_oc2o 8379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-un 3902  df-nul 4281  df-pr 4576  df-suc 6312  df-1o 8385  df-2o 8386

This theorem is referenced by:  df2o2  8394  2oex  8396  nlim2  8405  ord2eln012  8412  2oconcl  8418  enpr2d  8970  map2xp  9060  snnen2o  9129  rex2dom  9137  1sdom2dom  9138  cantnflem2  9580  xp2dju  10068  sdom2en01  10193  sadcf  16364  fnpr2o  17461  fnpr2ob  17462  fvprif  17465  xpsfrnel  17466  xpsfeq  17467  xpsle  17483  setcepi  17995  setc2obas  18001  setc2ohom  18002  efgi0  19632  efgi1  19633  vrgpf  19680  vrgpinv  19681  frgpuptinv  19683  frgpup2  19688  frgpup3lem  19689  frgpnabllem1  19785  dmdprdpr  19963  dprdpr  19964  xpstopnlem1  23724  xpstopnlem2  23726  xpsxmetlem  24294  xpsdsval  24296  xpsmet  24297  onint1  36493  pw2f1ocnv  43140  wepwsolem  43145  omnord1ex  43407  oege2  43410  df3o2  43416  oenord1ex  43418  oenord1  43419  oaomoencom  43420  oenassex  43421  omabs2  43435  omcl3g  43437  clsk1independent  44149  setc1onsubc  49713