Theorem df2o3 8457

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 8450	. 2 ⊢ 2o = suc 1o
2		df-suc 6366	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8456	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4118	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4592	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2789	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2790	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1570   ∪ cun 3903  ∅c0 4286  {csn 4589  {cpr 4591  suc csuc 6362  1_oc1o 8442  2_oc2o 8443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-un 3910  df-nul 4287  df-pr 4592  df-suc 6366  df-1o 8449  df-2o 8450

This theorem is referenced by:  df2o2  8458  2oex  8461  nlim2  8471  ord2eln012  8478  2oconcl  8484  enpr2d  9041  map2xp  9131  snnen2o  9201  rex2dom  9209  1sdom2dom  9210  cantnflem2  9655  xp2dju  10156  sdom2en01  10281  sadcf  16506  fnpr2o  17606  fnpr2ob  17607  fvprif  17610  xpsfrnel  17611  xpsfeq  17612  xpsle  17628  setcepi  18140  setc2obas  18146  setc2ohom  18147  efgi0  19785  efgi1  19786  vrgpf  19833  vrgpinv  19834  frgpuptinv  19836  frgpup2  19841  frgpup3lem  19842  frgpnabllem1  19938  dmdprdpr  20116  dprdpr  20117  xpstopnlem1  23966  xpstopnlem2  23968  xpsxmetlem  24536  xpsdsval  24538  xpsmet  24539  bdaypw2n0bndlem  28656  onint1  36980  pw2f1ocnv  43784  wepwsolem  43789  omnord1ex  44051  oege2  44054  df3o2  44060  oenord1ex  44062  oenord1  44063  oaomoencom  44064  oenassex  44065  omabs2  44079  omcl3g  44081  clsk1independent  44792  setc1onsubc  50400