Theorem df2o3 8119

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 8105	. 2 ⊢ 2o = suc 1o
2		df-suc 6199	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8118	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4137	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4572	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2849	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2850	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1537   ∪ cun 3936  ∅c0 4293  {csn 4569  {cpr 4571  suc csuc 6195  1_oc1o 8097  2_oc2o 8098

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-un 3943  df-nul 4294  df-pr 4572  df-suc 6199  df-1o 8104  df-2o 8105

This theorem is referenced by:  df2o2  8120  2oconcl  8130  map2xp  8689  1sdom  8723  cantnflem2  9155  xp2dju  9604  sdom2en01  9726  sadcf  15804  fnpr2o  16832  fnpr2ob  16833  fvprif  16836  xpsfrnel  16837  xpsfeq  16838  xpsle  16854  setcepi  17350  efgi0  18848  efgi1  18849  vrgpf  18896  vrgpinv  18897  frgpuptinv  18899  frgpup2  18904  frgpup3lem  18905  frgpnabllem1  18995  dmdprdpr  19173  dprdpr  19174  xpstopnlem1  22419  xpstopnlem2  22421  xpsxmetlem  22991  xpsdsval  22993  xpsmet  22994  onint1  33799  pw2f1ocnv  39641  wepwsolem  39649  df3o2  40381  clsk1independent  40403