NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  addccom Unicode version

Theorem addccom 4406
Description: Cardinal sum commutes. Theorem X.1.9 of [Rosser] p. 276. (Contributed by SF, 15-Jan-2015.)
Assertion
Ref Expression
addccom

Proof of Theorem addccom
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 incom 3448 . . . . . . 7
21eqeq1i 2360 . . . . . 6
3 uncom 3408 . . . . . . 7
43eqeq2i 2363 . . . . . 6
52, 4anbi12i 678 . . . . 5
652rexbii 2641 . . . 4
7 rexcom 2772 . . . 4
86, 7bitri 240 . . 3
98abbii 2465 . 2
10 df-addc 4378 . 2
11 df-addc 4378 . 2
129, 10, 113eqtr4i 2383 1
Colors of variables: wff setvar class
Syntax hints:   wa 358   wceq 1642  cab 2339  wrex 2615   cun 3207   cin 3208  c0 3550   cplc 4375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-rex 2620  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-addc 4378
This theorem is referenced by:  addcid2  4407  1cnnc  4408  addc32  4416  nncaddccl  4419  addcnnul  4453  ltfintr  4459  tfinltfinlem1  4500  oddtfin  4518  addccan1  4560  leaddc2  6215  nc0suc  6217  nmembers1lem3  6270  nchoicelem1  6289  nchoicelem7  6295  nchoicelem14  6302  nchoicelem17  6305
  Copyright terms: Public domain W3C validator