Theorem df2o3 6431

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 6418	. 2 ⊢ 2o = suc 1o
2		df-suc 4372	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 6430	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 3286	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 3600	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2201	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2202	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1353   ∪ cun 3128  ∅c0 3423  {csn 3593  {cpr 3594  suc csuc 4366  1_oc1o 6410  2_oc2o 6411

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-dif 3132  df-un 3134  df-nul 3424  df-pr 3600  df-suc 4372  df-1o 6417  df-2o 6418

This theorem is referenced by:  df2o2  6432  2oconcl  6440  0lt2o  6442  1lt2o  6443  el2oss1o  6444  en2eqpr  6907  nninfisol  7131  finomni  7138  exmidomniim  7139  exmidomni  7140  ismkvnex  7153  nninfwlpoimlemginf  7174  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  xp2dju  7214  pw1nel3  7230  sucpw1nel3  7232  unct  12443  fnpr2o  12758  fnpr2ob  12759  fvprif  12762  xpsfrnel  12763  xpsfeq  12764  2o01f  14749  nninfalllem1  14760  nninfall  14761  nninfsellemqall  14767  nninfomnilem  14770