Theorem df2o3 8403

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 8396	. 2 ⊢ 2o = suc 1o
2		df-suc 6316	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8402	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4094	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4558	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2765	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2766	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1547   ∪ cun 3881  ∅c0 4261  {csn 4555  {cpr 4557  suc csuc 6312  1_oc1o 8388  2_oc2o 8389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-un 3888  df-nul 4262  df-pr 4558  df-suc 6316  df-1o 8395  df-2o 8396

This theorem is referenced by:  df2o2  8404  2oex  8406  nlim2  8415  ord2eln012  8422  2oconcl  8428  enpr2d  8985  map2xp  9075  snnen2o  9145  rex2dom  9153  1sdom2dom  9154  cantnflem2  9602  xp2dju  10090  sdom2en01  10215  sadcf  16413  fnpr2o  17512  fnpr2ob  17513  fvprif  17516  xpsfrnel  17517  xpsfeq  17518  xpsle  17534  setcepi  18046  setc2obas  18052  setc2ohom  18053  efgi0  19686  efgi1  19687  vrgpf  19734  vrgpinv  19735  frgpuptinv  19737  frgpup2  19742  frgpup3lem  19743  frgpnabllem1  19839  dmdprdpr  20017  dprdpr  20018  xpstopnlem1  23792  xpstopnlem2  23794  xpsxmetlem  24362  xpsdsval  24364  xpsmet  24365  bdaypw2n0bndlem  28473  onint1  36677  pw2f1ocnv  43482  wepwsolem  43487  omnord1ex  43749  oege2  43752  df3o2  43758  oenord1ex  43760  oenord1  43761  oaomoencom  43762  oenassex  43763  omabs2  43777  omcl3g  43779  clsk1independent  44490  setc1onsubc  50092