ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df2o3 GIF version

Theorem df2o3 6425
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
StepHypRef Expression
1 df-2o 6412 . 2 2o = suc 1o
2 df-suc 4368 . 2 suc 1o = (1o ∪ {1o})
3 df1o2 6424 . . . 4 1o = {∅}
43uneq1i 3285 . . 3 (1o ∪ {1o}) = ({∅} ∪ {1o})
5 df-pr 3598 . . 3 {∅, 1o} = ({∅} ∪ {1o})
64, 5eqtr4i 2201 . 2 (1o ∪ {1o}) = {∅, 1o}
71, 2, 63eqtri 2202 1 2o = {∅, 1o}
Colors of variables: wff set class
Syntax hints:   = wceq 1353  cun 3127  c0 3422  {csn 3591  {cpr 3592  suc csuc 4362  1oc1o 6404  2oc2o 6405
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 2739  df-dif 3131  df-un 3133  df-nul 3423  df-pr 3598  df-suc 4368  df-1o 6411  df-2o 6412
This theorem is referenced by:  df2o2  6426  2oconcl  6434  0lt2o  6436  1lt2o  6437  el2oss1o  6438  en2eqpr  6901  nninfisol  7125  finomni  7132  exmidomniim  7133  exmidomni  7134  ismkvnex  7147  nninfwlpoimlemginf  7168  exmidfodomrlemr  7195  exmidfodomrlemrALT  7196  xp2dju  7208  pw1nel3  7224  sucpw1nel3  7226  unct  12423  2o01f  14399  nninfalllem1  14410  nninfall  14411  nninfsellemqall  14417  nninfomnilem  14420
  Copyright terms: Public domain W3C validator