Theorem df2o3 6597

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 6583	. 2 ⊢ 2o = suc 1o
2		df-suc 4468	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 6596	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 3357	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 3676	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2255	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2256	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1397   ∪ cun 3198  ∅c0 3494  {csn 3669  {cpr 3670  suc csuc 4462  1_oc1o 6575  2_oc2o 6576

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-dif 3202  df-un 3204  df-nul 3495  df-pr 3676  df-suc 4468  df-1o 6582  df-2o 6583

This theorem is referenced by:  df2o2  6598  2oex  6599  2oconcl  6607  0lt2o  6609  1lt2o  6610  el2oss1o  6611  rex2dom  6996  en2  6998  en2eqpr  7099  nninfisol  7332  finomni  7339  exmidomniim  7340  exmidomni  7341  ismkvnex  7354  nninfwlpoimlemginf  7375  pr2cv1  7400  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  xp2dju  7430  pw1nel3  7449  sucpw1nel3  7451  nninfctlemfo  12616  unct  13068  fnpr2o  13427  fnpr2ob  13428  fvprif  13431  xpsfrnel  13432  xpsfeq  13433  2o01f  16619  2omap  16620  nninfalllem1  16636  nninfall  16637  nninfsellemqall  16643  nninfomnilem  16646  nnnninfex  16650  nninfnfiinf  16651