Definition df-addc 4378

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

Assertion

Ref	Expression
df-addc	|- (A +o B) = {x | E.y e. A E.z e. B ((y i^i z) = (/) /\ x = (y u. z))}

Distinct variable groups:   x,A,y,z   x,B,y,z

Detailed syntax breakdown of Definition df-addc

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cplc 4375	. 2 class (A +o B)
4		vy	. . . . . . . . 9 setvar y
5	4	cv 1641	. . . . . . . 8 class y
6		vz	. . . . . . . . 9 setvar z
7	6	cv 1641	. . . . . . . 8 class z
8	5, 7	cin 3208	. . . . . . 7 class (y i^i z)
9		c0 3550	. . . . . . 7 class (/)
10	8, 9	wceq 1642	. . . . . 6 wff (y i^i z) = (/)
11		vx	. . . . . . . 8 setvar x
12	11	cv 1641	. . . . . . 7 class x
13	5, 7	cun 3207	. . . . . . 7 class (y u. z)
14	12, 13	wceq 1642	. . . . . 6 wff x = (y u. z)
15	10, 14	wa 358	. . . . 5 wff ((y i^i z) = (/) /\ x = (y u. z))
16	15, 6, 2	wrex 2615	. . . 4 wff E.z e. B ((y i^i z) = (/) /\ x = (y u. z))
17	16, 4, 1	wrex 2615	. . 3 wff E.y e. A E.z e. B ((y i^i z) = (/) /\ x = (y u. z))
18	17, 11	cab 2339	. 2 class {x | E.y e. A E.z e. B ((y i^i z) = (/) /\ x = (y u. z))}
19	3, 18	wceq 1642	1 wff (A +o B) = {x | E.y e. A E.z e. B ((y i^i z) = (/) /\ x = (y u. z))}

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