Definition df-addc 4379

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 ((y ∩ z) = ∅ ∧ x = (y ∪ 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 4376	. 2 class (A +c 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 3209	. . . . . . 7 class (y ∩ z)
9		c0 3551	. . . . . . 7 class ∅
10	8, 9	wceq 1642	. . . . . 6 wff (y ∩ z) = ∅
11		vx	. . . . . . . 8 setvar x
12	11	cv 1641	. . . . . . 7 class x
13	5, 7	cun 3208	. . . . . . 7 class (y ∪ z)
14	12, 13	wceq 1642	. . . . . 6 wff x = (y ∪ z)
15	10, 14	wa 358	. . . . 5 wff ((y ∩ z) = ∅ ∧ x = (y ∪ z))
16	15, 6, 2	wrex 2616	. . . 4 wff ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))
17	16, 4, 1	wrex 2616	. . 3 wff ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))
18	17, 11	cab 2339	. 2 class {x ∣ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))}
19	3, 18	wceq 1642	1 wff (A +c B) = {x ∣ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))}

This definition is referenced by:  dfaddc2  4382  eladdc  4399  addccom  4407  ltfinex  4465  evenodddisjlem1  4516