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

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

Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 incom 3448 . . . . . . 7 (yz) = (zy)
21eqeq1i 2360 . . . . . 6 ((yz) = ↔ (zy) = )
3 uncom 3408 . . . . . . 7 (yz) = (zy)
43eqeq2i 2363 . . . . . 6 (x = (yz) ↔ x = (zy))
52, 4anbi12i 678 . . . . 5 (((yz) = x = (yz)) ↔ ((zy) = x = (zy)))
652rexbii 2641 . . . 4 (y A z B ((yz) = x = (yz)) ↔ y A z B ((zy) = x = (zy)))
7 rexcom 2772 . . . 4 (y A z B ((zy) = x = (zy)) ↔ z B y A ((zy) = x = (zy)))
86, 7bitri 240 . . 3 (y A z B ((yz) = x = (yz)) ↔ z B y A ((zy) = x = (zy)))
98abbii 2465 . 2 {x y A z B ((yz) = x = (yz))} = {x z B y A ((zy) = x = (zy))}
10 df-addc 4378 . 2 (A +c B) = {x y A z B ((yz) = x = (yz))}
11 df-addc 4378 . 2 (B +c A) = {x z B y A ((zy) = x = (zy))}
129, 10, 113eqtr4i 2383 1 (A +c B) = (B +c A)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 358   = wceq 1642  {cab 2339  ∃wrex 2615   ∪ cun 3207   ∩ cin 3208  ∅c0 3550   +c cplc 4375 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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