Definition df-cda 3715

Description: Define cardinal number addition. Definition of cardinal sum in [Mendelson] p. 258. See cdaval 3717 for its value and a description.

Assertion

Ref	Expression
df-cda	|- +c = {<.<.x, y>., z>. | z = ((x X. {(/)}) u. (y X. {1o}))}

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-cda

Step	Hyp	Ref	Expression
1		ccda 3714	. 2 class +c
2		vz	. . . . 5 set z
3	2	cv 1089	. . . 4 class z
4		vx	. . . . . . 7 set x
5	4	cv 1089	. . . . . 6 class x
6		c0 1707	. . . . . . 7 class (/)
7	6	csn 1808	. . . . . 6 class {(/)}
8	5, 7	cxp 2408	. . . . 5 class (x X. {(/)})
9		vy	. . . . . . 7 set y
10	9	cv 1089	. . . . . 6 class y
11		c1o 3099	. . . . . . 7 class 1o
12	11	csn 1808	. . . . . 6 class {1o}
13	10, 12	cxp 2408	. . . . 5 class (y X. {1o})
14	8, 13	cun 1485	. . . 4 class ((x X. {(/)}) u. (y X. {1o}))
15	3, 14	wceq 1091	. . 3 wff z = ((x X. {(/)}) u. (y X. {1o}))
16	15, 4, 9, 2	copab2 3002	. 2 class {<.<.x, y>., z>. | z = ((x X. {(/)}) u. (y X. {1o}))}
17	1, 16	wceq 1091	1 wff +c = {<.<.x, y>., z>. | z = ((x X. {(/)}) u. (y X. {1o}))}

This definition is referenced by:  cdavalt 3716

metamath.org