Theorem df2o3 8515

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 8508	. 2 ⊢ 2o = suc 1o
2		df-suc 6389	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8514	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4163	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4628	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2767	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2768	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1539   ∪ cun 3948  ∅c0 4332  {csn 4625  {cpr 4627  suc csuc 6385  1_oc1o 8500  2_oc2o 8501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-dif 3953  df-un 3955  df-nul 4333  df-pr 4628  df-suc 6389  df-1o 8507  df-2o 8508

This theorem is referenced by:  df2o2  8516  2oex  8518  nlim2  8529  ord2eln012  8536  2oconcl  8542  enpr2d  9090  map2xp  9188  snnen2o  9274  rex2dom  9283  1sdom2dom  9284  1sdomOLD  9286  cantnflem2  9731  xp2dju  10218  sdom2en01  10343  sadcf  16491  fnpr2o  17603  fnpr2ob  17604  fvprif  17607  xpsfrnel  17608  xpsfeq  17609  xpsle  17625  setcepi  18134  setc2obas  18140  setc2ohom  18141  efgi0  19739  efgi1  19740  vrgpf  19787  vrgpinv  19788  frgpuptinv  19790  frgpup2  19795  frgpup3lem  19796  frgpnabllem1  19892  dmdprdpr  20070  dprdpr  20071  xpstopnlem1  23818  xpstopnlem2  23820  xpsxmetlem  24390  xpsdsval  24392  xpsmet  24393  onint1  36451  pw2f1ocnv  43054  wepwsolem  43059  omnord1ex  43322  oege2  43325  df3o2  43331  oenord1ex  43333  oenord1  43334  oaomoencom  43335  oenassex  43336  omabs2  43350  omcl3g  43352  clsk1independent  44064