Theorem df2o3 8407

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 8400	. 2 ⊢ 2o = suc 1o
2		df-suc 6324	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8406	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4105	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4571	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2763	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2764	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1542   ∪ cun 3888  ∅c0 4274  {csn 4568  {cpr 4570  suc csuc 6320  1_oc1o 8392  2_oc2o 8393

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-un 3895  df-nul 4275  df-pr 4571  df-suc 6324  df-1o 8399  df-2o 8400

This theorem is referenced by:  df2o2  8408  2oex  8410  nlim2  8419  ord2eln012  8426  2oconcl  8432  enpr2d  8989  map2xp  9079  snnen2o  9149  rex2dom  9157  1sdom2dom  9158  cantnflem2  9605  xp2dju  10093  sdom2en01  10218  sadcf  16416  fnpr2o  17515  fnpr2ob  17516  fvprif  17519  xpsfrnel  17520  xpsfeq  17521  xpsle  17537  setcepi  18049  setc2obas  18055  setc2ohom  18056  efgi0  19689  efgi1  19690  vrgpf  19737  vrgpinv  19738  frgpuptinv  19740  frgpup2  19745  frgpup3lem  19746  frgpnabllem1  19842  dmdprdpr  20020  dprdpr  20021  xpstopnlem1  23787  xpstopnlem2  23789  xpsxmetlem  24357  xpsdsval  24359  xpsmet  24360  bdaypw2n0bndlem  28472  onint1  36650  pw2f1ocnv  43486  wepwsolem  43491  omnord1ex  43753  oege2  43756  df3o2  43762  oenord1ex  43764  oenord1  43765  oaomoencom  43766  oenassex  43767  omabs2  43781  omcl3g  43783  clsk1independent  44494  setc1onsubc  50092