Theorem df2o3 6515

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 6502	. 2 ⊢ 2o = suc 1o
2		df-suc 4417	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 6514	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 3322	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 3639	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2228	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2229	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1372   ∪ cun 3163  ∅c0 3459  {csn 3632  {cpr 3633  suc csuc 4411  1_oc1o 6494  2_oc2o 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-dif 3167  df-un 3169  df-nul 3460  df-pr 3639  df-suc 4417  df-1o 6501  df-2o 6502

This theorem is referenced by:  df2o2  6516  2oconcl  6524  0lt2o  6526  1lt2o  6527  el2oss1o  6528  rex2dom  6909  en2  6911  en2eqpr  7003  nninfisol  7234  finomni  7241  exmidomniim  7242  exmidomni  7243  ismkvnex  7256  nninfwlpoimlemginf  7277  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  xp2dju  7326  pw1nel3  7342  sucpw1nel3  7344  nninfctlemfo  12303  unct  12755  fnpr2o  13113  fnpr2ob  13114  fvprif  13117  xpsfrnel  13118  xpsfeq  13119  2o01f  15864  2omap  15865  nninfalllem1  15878  nninfall  15879  nninfsellemqall  15885  nninfomnilem  15888  nnnninfex  15892  nninfnfiinf  15893