Theorem df2o3 6696

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 6682	. 2 ⊢ 2o = suc 1o
2		df-suc 4514	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 6695	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 3379	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 3715	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2262	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2263	1 ⊢ 2o = {∅, 1o}

This proof depends on syntax axioms:   = wceq 1402   ∪ cun 3218  ∅c0 3520  {csn 3708  {cpr 3709  suc csuc 4508  1_oc1o 6674  2_oc2o 6675

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-dif 3222  df-un 3224  df-nul 3521  df-pr 3715  df-suc 4514  df-1o 6681  df-2o 6682

This theorem is used by:  df2o2  6697  2oex  6698  2oconcl  6706  0lt2o  6708  1lt2o  6709  el2oss1o  6710  rex2dom  7104  en2  7106  en2eqpr  7208  2omap  7312  nninfisol  7467  finomni  7474  exmidomniim  7475  exmidomni  7476  ismkvnex  7489  nninfwlpoimlemginf  7510  pr2cv1  7535  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  xp2dju  7565  pw1nel3  7584  sucpw1nel3  7586  nninfctlemfo  12800  unct  13316  fnpr2o  13643  fnpr2ob  13644  fvprif  13647  xpsfrnel  13648  xpsfeq  13649  2o01f  17007  nninfalllem1  17026  nninfall  17027  nninfsellemqall  17033  nninfomnilem  17036  nnnninfex  17040  nninfnfiinf  17041