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

 Description: Define cardinal addition. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
df-addc (A +c B) = {x y A z B ((yz) = x = (yz))}
Distinct variable groups:   x,A,y,z   x,B,y,z

Detailed syntax breakdown of Definition df-addc
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cplc 4375 . 2 class (A +c B)
4 vy . . . . . . . . 9 setvar y
54cv 1641 . . . . . . . 8 class y
6 vz . . . . . . . . 9 setvar z
76cv 1641 . . . . . . . 8 class z
85, 7cin 3208 . . . . . . 7 class (yz)
9 c0 3550 . . . . . . 7 class
108, 9wceq 1642 . . . . . 6 wff (yz) =
11 vx . . . . . . . 8 setvar x
1211cv 1641 . . . . . . 7 class x
135, 7cun 3207 . . . . . . 7 class (yz)
1412, 13wceq 1642 . . . . . 6 wff x = (yz)
1510, 14wa 358 . . . . 5 wff ((yz) = x = (yz))
1615, 6, 2wrex 2615 . . . 4 wff z B ((yz) = x = (yz))
1716, 4, 1wrex 2615 . . 3 wff y A z B ((yz) = x = (yz))
1817, 11cab 2339 . 2 class {x y A z B ((yz) = x = (yz))}
193, 18wceq 1642 1 wff (A +c B) = {x y A z B ((yz) = x = (yz))}
 Colors of variables: wff setvar class This definition is referenced by:  dfaddc2  4381  eladdc  4398  addccom  4406  ltfinex  4464  evenodddisjlem1  4515
 Copyright terms: Public domain W3C validator