Theorem df2o3 8117

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 8103	. 2 ⊢ 2o = suc 1o
2		df-suc 6197	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8116	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4135	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4570	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2847	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2848	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1537   ∪ cun 3934  ∅c0 4291  {csn 4567  {cpr 4569  suc csuc 6193  1_oc1o 8095  2_oc2o 8096

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-un 3941  df-nul 4292  df-pr 4570  df-suc 6197  df-1o 8102  df-2o 8103

This theorem is referenced by:  df2o2  8118  2oconcl  8128  map2xp  8687  1sdom  8721  cantnflem2  9153  xp2dju  9602  sdom2en01  9724  sadcf  15802  fnpr2o  16830  fnpr2ob  16831  fvprif  16834  xpsfrnel  16835  xpsfeq  16836  xpsle  16852  setcepi  17348  efgi0  18846  efgi1  18847  vrgpf  18894  vrgpinv  18895  frgpuptinv  18897  frgpup2  18902  frgpup3lem  18903  frgpnabllem1  18993  dmdprdpr  19171  dprdpr  19172  xpstopnlem1  22417  xpstopnlem2  22419  xpsxmetlem  22989  xpsdsval  22991  xpsmet  22992  onint1  33797  pw2f1ocnv  39654  wepwsolem  39662  df3o2  40394  clsk1independent  40416