NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  1p1e2c GIF version

Theorem 1p1e2c 5368
Description: One plus one equals two. Theorem *110.64 of {{WhiteheadRussell}}. This theorem is occasionally useful.
Assertion
Ref Expression
1p1e2c (1c +c 1c) = 2c

Proof of Theorem 1p1e2c
StepHypRef Expression
1 0ex 3212 . . . . . 6 V
2 n0i 2732 . . . . . 6 ( V → ¬ V = )
31, 2ax-mp 8 . . . . 5 ¬ V =
4 vvex 3211 . . . . . 6 V V
54elsn 2836 . . . . 5 (V {} ↔ V = )
63, 5mtbir 287 . . . 4 ¬ V {}
7 disjsn 2860 . . . 4 (({} ∩ {V}) = ↔ ¬ V {})
86, 7mpbir 197 . . 3 ({} ∩ {V}) =
9 snex 3213 . . . 4 {} V
10 snex 3213 . . . 4 {V} V
119, 10ncdisjun 5349 . . 3 (({} ∩ {V}) = Nc ({} ∪ {V}) = ( Nc {} +c Nc {V}))
128, 11ax-mp 8 . 2 Nc ({} ∪ {V}) = ( Nc {} +c Nc {V})
13 df-2c 5316 . . 3 2c = Nc {, V}
14 df-pr 2808 . . . 4 {, V} = ({} ∪ {V})
1514nceqi 5321 . . 3 Nc {, V} = Nc ({} ∪ {V})
1613, 15eqtri 1915 . 2 2c = Nc ({} ∪ {V})
171df1c3 5353 . . 3 1c = Nc {}
184df1c3 5353 . . 3 1c = Nc {V}
1917, 18addceq12i 3496 . 2 (1c +c 1c) = ( Nc {} +c Nc {V})
2012, 16, 193eqtr4ri 1926 1 (1c +c 1c) = 2c
Colors of variables: wff set class
Syntax hints:  ¬ wn 3   = wceq 1398   wcel 1400  Vcvv 2300  cun 2609  cin 2610  c0 2726  {csn 2803  {cpr 2804  1cc1c 3238   +c cplc 3483   Nc cnc 5303  2cc2c 5306
This theorem is referenced by:  tc2c  5379  2nnc  5380  el2c  5404  2ne0c  5454  nncdiv3  5469  nnc3n3p2  5471  nnc3p1n3p2  5472  nchoicelem1  5481  nchoicelem2  5482  nchoicelem9  5489  nchoicelem17  5497
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1323  ax-6 1324  ax-7 1325  ax-gen 1326  ax-8 1402  ax-10 1403  ax-11 1404  ax-12 1405  ax-13 1406  ax-14 1407  ax-17 1413  ax-9 1424  ax-4 1429  ax-16 1606  ax-ext 1877  ax-nin 3180  ax-xp 3181  ax-cnv 3182  ax-1c 3183  ax-sset 3184  ax-si 3185  ax-ins2 3186  ax-ins3 3187  ax-typlower 3188  ax-sn 3189
This theorem depends on definitions:  df-bi 174  df-or 356  df-an 357  df-3or 885  df-3an 886  df-nand 1259  df-tru 1301  df-ex 1328  df-sb 1568  df-eu 1795  df-mo 1796  df-clab 1883  df-cleq 1888  df-clel 1891  df-ne 2014  df-ral 2107  df-rex 2108  df-reu 2109  df-rab 2110  df-v 2302  df-sbc 2469  df-nin 2613  df-compl 2614  df-in 2615  df-un 2616  df-dif 2617  df-symdif 2618  df-nul 2727  df-sn 2807  df-pr 2808  df-opk 2863  df-ss 2876  df-pss 2878  df-uni 3038  df-int 3072  df-if 3109  df-pw 3167  df-1c 3240  df-pw1 3241  df-uni1 3242  df-xpk 3289  df-cnvk 3290  df-ins2k 3291  df-ins3k 3292  df-imak 3293  df-cok 3294  df-p6 3295  df-sik 3296  df-ssetk 3297  df-imagek 3298  df-idk 3299  df-iota 3450  df-0c 3485  df-addc 3486  df-nnc 3487  df-fin 3488  df-lefin 3547  df-ltfin 3548  df-ncfin 3549  df-tfin 3550  df-evenfin 3551  df-oddfin 3552  df-sfin 3553  df-spfin 3554  df-phi 3673  df-op 3674  df-proj1 3675  df-proj2 3676  df-opab 3723  df-br 3737  df-1st 3821  df-swap 3822  df-sset 3823  df-co 3824  df-ima 3825  df-si 3826  df-id 3939  df-xp 3957  df-rel 3958  df-cnv 3959  df-rn 3960  df-dm 3961  df-res 3962  df-fun 3963  df-fn 3964  df-f 3965  df-f1 3966  df-fo 3967  df-f1o 3968  df-fv 3969  df-2nd 3971  df-txp 4978  df-ins2 4984  df-ins3 4985  df-image 4986  df-ins4 4987  df-si3 4988  df-funs 4989  df-fns 4990  df-trans 5110  df-sym 5119  df-er 5120  df-ec 5158  df-qs 5162  df-en 5241  df-ncs 5310  df-nc 5313  df-2c 5316
  Copyright terms: Public domain W3C validator