Theorem df2o3 8480

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 8473	. 2 ⊢ 2o = suc 1o
2		df-suc 6370	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8479	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4159	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4631	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2762	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2763	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1540   ∪ cun 3946  ∅c0 4322  {csn 4628  {cpr 4630  suc csuc 6366  1_oc1o 8465  2_oc2o 8466

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-dif 3951  df-un 3953  df-nul 4323  df-pr 4631  df-suc 6370  df-1o 8472  df-2o 8473

This theorem is referenced by:  df2o2  8481  2oex  8483  nlim2  8496  ord2eln012  8503  2oconcl  8509  enpr2d  9055  map2xp  9153  snnen2o  9243  rex2dom  9252  1sdom2dom  9253  1sdomOLD  9255  cantnflem2  9691  xp2dju  10177  sdom2en01  10303  sadcf  16401  fnpr2o  17510  fnpr2ob  17511  fvprif  17514  xpsfrnel  17515  xpsfeq  17516  xpsle  17532  setcepi  18048  setc2obas  18054  setc2ohom  18055  efgi0  19636  efgi1  19637  vrgpf  19684  vrgpinv  19685  frgpuptinv  19687  frgpup2  19692  frgpup3lem  19693  frgpnabllem1  19789  dmdprdpr  19967  dprdpr  19968  xpstopnlem1  23633  xpstopnlem2  23635  xpsxmetlem  24205  xpsdsval  24207  xpsmet  24208  onint1  35798  pw2f1ocnv  42239  wepwsolem  42247  omnord1ex  42517  oege2  42520  df3o2  42526  oenord1ex  42528  oenord1  42529  oaomoencom  42530  oenassex  42531  omabs2  42545  omcl3g  42547  clsk1independent  43260