df-addc - New Foundations Explorer

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

Definition df-addc 4378

Description: Define cardinal addition. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.)

**Assertion**
Ref	Expression
df-addc	$/\$

**Detailed syntax breakdown of Definition df-addc**
Step	Hyp	Ref	Expression
1		cA	. . 3
2		cB	. . 3
3	1, 2	cplc 4375	. 2
4		vy	. . . . . . . . 9
5	4	cv 1641	. . . . . . . 8
6		vz	. . . . . . . . 9
7	6	cv 1641	. . . . . . . 8
8	5, 7	cin 3208	. . . . . . 7
9		c0 3550	. . . . . . 7
10	8, 9	wceq 1642	. . . . . 6
11		vx	. . . . . . . 8
12	11	cv 1641	. . . . . . 7
13	5, 7	cun 3207	. . . . . . 7
14	12, 13	wceq 1642	. . . . . 6
15	10, 14	wa 358	. . . . 5 $/\$
16	15, 6, 2	wrex 2615	. . . 4 $/\$
17	16, 4, 1	wrex 2615	. . 3 $/\$
18	17, 11	cab 2339	. 2 $/\$
19	3, 18	wceq 1642	1 $/\$

Colors of variables: wff setvar class

This definition is referenced by: dfaddc2 4381 eladdc 4398 addccom 4406 ltfinex 4464 evenodddisjlem1 4515