Theorem addcass 4415

Description: Cardinal addition is associative. Theorem X.1.11, corollary 1 of [Rosser] p. 277. (Contributed by SF, 17-Jan-2015.)

Assertion

Ref	Expression
addcass	⊢ ((A +c B) +c C) = (A +c (B +c C))

Proof of Theorem addcass

Dummy variables a b c d e x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ancom 437	. . . . . . . . . . 11 ⊢ (((a ∩ c) = ∅ ∧ (b ∩ c) = ∅) ↔ ((b ∩ c) = ∅ ∧ (a ∩ c) = ∅))
2	1	anbi2i 675	. . . . . . . . . 10 ⊢ (((a ∩ b) = ∅ ∧ ((a ∩ c) = ∅ ∧ (b ∩ c) = ∅)) ↔ ((a ∩ b) = ∅ ∧ ((b ∩ c) = ∅ ∧ (a ∩ c) = ∅)))
3		an12 772	. . . . . . . . . 10 ⊢ (((a ∩ b) = ∅ ∧ ((b ∩ c) = ∅ ∧ (a ∩ c) = ∅)) ↔ ((b ∩ c) = ∅ ∧ ((a ∩ b) = ∅ ∧ (a ∩ c) = ∅)))
4	2, 3	bitri 240	. . . . . . . . 9 ⊢ (((a ∩ b) = ∅ ∧ ((a ∩ c) = ∅ ∧ (b ∩ c) = ∅)) ↔ ((b ∩ c) = ∅ ∧ ((a ∩ b) = ∅ ∧ (a ∩ c) = ∅)))
5		indir 3503	. . . . . . . . . . . 12 ⊢ ((a ∪ b) ∩ c) = ((a ∩ c) ∪ (b ∩ c))
6	5	eqeq1i 2360	. . . . . . . . . . 11 ⊢ (((a ∪ b) ∩ c) = ∅ ↔ ((a ∩ c) ∪ (b ∩ c)) = ∅)
7		un00 3586	. . . . . . . . . . 11 ⊢ (((a ∩ c) = ∅ ∧ (b ∩ c) = ∅) ↔ ((a ∩ c) ∪ (b ∩ c)) = ∅)
8	6, 7	bitr4i 243	. . . . . . . . . 10 ⊢ (((a ∪ b) ∩ c) = ∅ ↔ ((a ∩ c) = ∅ ∧ (b ∩ c) = ∅))
9	8	anbi2i 675	. . . . . . . . 9 ⊢ (((a ∩ b) = ∅ ∧ ((a ∪ b) ∩ c) = ∅) ↔ ((a ∩ b) = ∅ ∧ ((a ∩ c) = ∅ ∧ (b ∩ c) = ∅)))
10		indi 3501	. . . . . . . . . . . 12 ⊢ (a ∩ (b ∪ c)) = ((a ∩ b) ∪ (a ∩ c))
11	10	eqeq1i 2360	. . . . . . . . . . 11 ⊢ ((a ∩ (b ∪ c)) = ∅ ↔ ((a ∩ b) ∪ (a ∩ c)) = ∅)
12		un00 3586	. . . . . . . . . . 11 ⊢ (((a ∩ b) = ∅ ∧ (a ∩ c) = ∅) ↔ ((a ∩ b) ∪ (a ∩ c)) = ∅)
13	11, 12	bitr4i 243	. . . . . . . . . 10 ⊢ ((a ∩ (b ∪ c)) = ∅ ↔ ((a ∩ b) = ∅ ∧ (a ∩ c) = ∅))
14	13	anbi2i 675	. . . . . . . . 9 ⊢ (((b ∩ c) = ∅ ∧ (a ∩ (b ∪ c)) = ∅) ↔ ((b ∩ c) = ∅ ∧ ((a ∩ b) = ∅ ∧ (a ∩ c) = ∅)))
15	4, 9, 14	3bitr4i 268	. . . . . . . 8 ⊢ (((a ∩ b) = ∅ ∧ ((a ∪ b) ∩ c) = ∅) ↔ ((b ∩ c) = ∅ ∧ (a ∩ (b ∪ c)) = ∅))
16		unass 3420	. . . . . . . . 9 ⊢ ((a ∪ b) ∪ c) = (a ∪ (b ∪ c))
17	16	eqeq2i 2363	. . . . . . . 8 ⊢ (x = ((a ∪ b) ∪ c) ↔ x = (a ∪ (b ∪ c)))
18	15, 17	anbi12i 678	. . . . . . 7 ⊢ ((((a ∩ b) = ∅ ∧ ((a ∪ b) ∩ c) = ∅) ∧ x = ((a ∪ b) ∪ c)) ↔ (((b ∩ c) = ∅ ∧ (a ∩ (b ∪ c)) = ∅) ∧ x = (a ∪ (b ∪ c))))
19		anass 630	. . . . . . 7 ⊢ ((((a ∩ b) = ∅ ∧ ((a ∪ b) ∩ c) = ∅) ∧ x = ((a ∪ b) ∪ c)) ↔ ((a ∩ b) = ∅ ∧ (((a ∪ b) ∩ c) = ∅ ∧ x = ((a ∪ b) ∪ c))))
20		anass 630	. . . . . . 7 ⊢ ((((b ∩ c) = ∅ ∧ (a ∩ (b ∪ c)) = ∅) ∧ x = (a ∪ (b ∪ c))) ↔ ((b ∩ c) = ∅ ∧ ((a ∩ (b ∪ c)) = ∅ ∧ x = (a ∪ (b ∪ c)))))
21	18, 19, 20	3bitr3i 266	. . . . . 6 ⊢ (((a ∩ b) = ∅ ∧ (((a ∪ b) ∩ c) = ∅ ∧ x = ((a ∪ b) ∪ c))) ↔ ((b ∩ c) = ∅ ∧ ((a ∩ (b ∪ c)) = ∅ ∧ x = (a ∪ (b ∪ c)))))
22		anass 630	. . . . . . . . 9 ⊢ ((((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ((a ∩ b) = ∅ ∧ (d = (a ∪ b) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c)))))
23		an12 772	. . . . . . . . 9 ⊢ (((a ∩ b) = ∅ ∧ (d = (a ∪ b) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c)))) ↔ (d = (a ∪ b) ∧ ((a ∩ b) = ∅ ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c)))))
24	22, 23	bitri 240	. . . . . . . 8 ⊢ ((((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ (d = (a ∪ b) ∧ ((a ∩ b) = ∅ ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c)))))
25	24	exbii 1582	. . . . . . 7 ⊢ (∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃d(d = (a ∪ b) ∧ ((a ∩ b) = ∅ ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c)))))
26		vex 2862	. . . . . . . . 9 ⊢ a ∈ V
27		vex 2862	. . . . . . . . 9 ⊢ b ∈ V
28	26, 27	unex 4106	. . . . . . . 8 ⊢ (a ∪ b) ∈ V
29		ineq1 3450	. . . . . . . . . . 11 ⊢ (d = (a ∪ b) → (d ∩ c) = ((a ∪ b) ∩ c))
30	29	eqeq1d 2361	. . . . . . . . . 10 ⊢ (d = (a ∪ b) → ((d ∩ c) = ∅ ↔ ((a ∪ b) ∩ c) = ∅))
31		uneq1 3411	. . . . . . . . . . 11 ⊢ (d = (a ∪ b) → (d ∪ c) = ((a ∪ b) ∪ c))
32	31	eqeq2d 2364	. . . . . . . . . 10 ⊢ (d = (a ∪ b) → (x = (d ∪ c) ↔ x = ((a ∪ b) ∪ c)))
33	30, 32	anbi12d 691	. . . . . . . . 9 ⊢ (d = (a ∪ b) → (((d ∩ c) = ∅ ∧ x = (d ∪ c)) ↔ (((a ∪ b) ∩ c) = ∅ ∧ x = ((a ∪ b) ∪ c))))
34	33	anbi2d 684	. . . . . . . 8 ⊢ (d = (a ∪ b) → (((a ∩ b) = ∅ ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ((a ∩ b) = ∅ ∧ (((a ∪ b) ∩ c) = ∅ ∧ x = ((a ∪ b) ∪ c)))))
35	28, 34	ceqsexv 2894	. . . . . . 7 ⊢ (∃d(d = (a ∪ b) ∧ ((a ∩ b) = ∅ ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c)))) ↔ ((a ∩ b) = ∅ ∧ (((a ∪ b) ∩ c) = ∅ ∧ x = ((a ∪ b) ∪ c))))
36	25, 35	bitri 240	. . . . . 6 ⊢ (∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ((a ∩ b) = ∅ ∧ (((a ∪ b) ∩ c) = ∅ ∧ x = ((a ∪ b) ∪ c))))
37		anass 630	. . . . . . . . 9 ⊢ ((((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ ((b ∩ c) = ∅ ∧ (e = (b ∪ c) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e)))))
38		an12 772	. . . . . . . . 9 ⊢ (((b ∩ c) = ∅ ∧ (e = (b ∪ c) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e)))) ↔ (e = (b ∪ c) ∧ ((b ∩ c) = ∅ ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e)))))
39	37, 38	bitri 240	. . . . . . . 8 ⊢ ((((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ (e = (b ∪ c) ∧ ((b ∩ c) = ∅ ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e)))))
40	39	exbii 1582	. . . . . . 7 ⊢ (∃e(((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ ∃e(e = (b ∪ c) ∧ ((b ∩ c) = ∅ ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e)))))
41		vex 2862	. . . . . . . . 9 ⊢ c ∈ V
42	27, 41	unex 4106	. . . . . . . 8 ⊢ (b ∪ c) ∈ V
43		ineq2 3451	. . . . . . . . . . 11 ⊢ (e = (b ∪ c) → (a ∩ e) = (a ∩ (b ∪ c)))
44	43	eqeq1d 2361	. . . . . . . . . 10 ⊢ (e = (b ∪ c) → ((a ∩ e) = ∅ ↔ (a ∩ (b ∪ c)) = ∅))
45		uneq2 3412	. . . . . . . . . . 11 ⊢ (e = (b ∪ c) → (a ∪ e) = (a ∪ (b ∪ c)))
46	45	eqeq2d 2364	. . . . . . . . . 10 ⊢ (e = (b ∪ c) → (x = (a ∪ e) ↔ x = (a ∪ (b ∪ c))))
47	44, 46	anbi12d 691	. . . . . . . . 9 ⊢ (e = (b ∪ c) → (((a ∩ e) = ∅ ∧ x = (a ∪ e)) ↔ ((a ∩ (b ∪ c)) = ∅ ∧ x = (a ∪ (b ∪ c)))))
48	47	anbi2d 684	. . . . . . . 8 ⊢ (e = (b ∪ c) → (((b ∩ c) = ∅ ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ ((b ∩ c) = ∅ ∧ ((a ∩ (b ∪ c)) = ∅ ∧ x = (a ∪ (b ∪ c))))))
49	42, 48	ceqsexv 2894	. . . . . . 7 ⊢ (∃e(e = (b ∪ c) ∧ ((b ∩ c) = ∅ ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e)))) ↔ ((b ∩ c) = ∅ ∧ ((a ∩ (b ∪ c)) = ∅ ∧ x = (a ∪ (b ∪ c)))))
50	40, 49	bitri 240	. . . . . 6 ⊢ (∃e(((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ ((b ∩ c) = ∅ ∧ ((a ∩ (b ∪ c)) = ∅ ∧ x = (a ∪ (b ∪ c)))))
51	21, 36, 50	3bitr4i 268	. . . . 5 ⊢ (∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃e(((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
52	51	rexbii 2639	. . . 4 ⊢ (∃c ∈ C ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃c ∈ C ∃e(((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
53	52	2rexbii 2641	. . 3 ⊢ (∃a ∈ A ∃b ∈ B ∃c ∈ C ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃a ∈ A ∃b ∈ B ∃c ∈ C ∃e(((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
54		eladdc 4398	. . . 4 ⊢ (x ∈ ((A +c B) +c C) ↔ ∃d ∈ (A +c B)∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c)))
55		df-rex 2620	. . . . 5 ⊢ (∃d ∈ (A +c B)∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c)) ↔ ∃d(d ∈ (A +c B) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
56		rexcom4 2878	. . . . . 6 ⊢ (∃a ∈ A ∃d∃b ∈ B (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃d∃a ∈ A ∃b ∈ B (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
57		rexcom4 2878	. . . . . . . . . 10 ⊢ (∃c ∈ C ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃d∃c ∈ C (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
58		r19.42v 2765	. . . . . . . . . . 11 ⊢ (∃c ∈ C (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
59	58	exbii 1582	. . . . . . . . . 10 ⊢ (∃d∃c ∈ C (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
60	57, 59	bitri 240	. . . . . . . . 9 ⊢ (∃c ∈ C ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
61	60	rexbii 2639	. . . . . . . 8 ⊢ (∃b ∈ B ∃c ∈ C ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃b ∈ B ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
62		rexcom4 2878	. . . . . . . 8 ⊢ (∃b ∈ B ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃d∃b ∈ B (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
63	61, 62	bitri 240	. . . . . . 7 ⊢ (∃b ∈ B ∃c ∈ C ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃d∃b ∈ B (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
64	63	rexbii 2639	. . . . . 6 ⊢ (∃a ∈ A ∃b ∈ B ∃c ∈ C ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃a ∈ A ∃d∃b ∈ B (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
65		r19.41v 2764	. . . . . . . 8 ⊢ (∃a ∈ A (∃b ∈ B ((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ (∃a ∈ A ∃b ∈ B ((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
66		r19.41v 2764	. . . . . . . . 9 ⊢ (∃b ∈ B (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ (∃b ∈ B ((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
67	66	rexbii 2639	. . . . . . . 8 ⊢ (∃a ∈ A ∃b ∈ B (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃a ∈ A (∃b ∈ B ((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
68		eladdc 4398	. . . . . . . . 9 ⊢ (d ∈ (A +c B) ↔ ∃a ∈ A ∃b ∈ B ((a ∩ b) = ∅ ∧ d = (a ∪ b)))
69	68	anbi1i 676	. . . . . . . 8 ⊢ ((d ∈ (A +c B) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ (∃a ∈ A ∃b ∈ B ((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
70	65, 67, 69	3bitr4ri 269	. . . . . . 7 ⊢ ((d ∈ (A +c B) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃a ∈ A ∃b ∈ B (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
71	70	exbii 1582	. . . . . 6 ⊢ (∃d(d ∈ (A +c B) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃d∃a ∈ A ∃b ∈ B (((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
72	56, 64, 71	3bitr4ri 269	. . . . 5 ⊢ (∃d(d ∈ (A +c B) ∧ ∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c))) ↔ ∃a ∈ A ∃b ∈ B ∃c ∈ C ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
73	55, 72	bitri 240	. . . 4 ⊢ (∃d ∈ (A +c B)∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c)) ↔ ∃a ∈ A ∃b ∈ B ∃c ∈ C ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
74	54, 73	bitri 240	. . 3 ⊢ (x ∈ ((A +c B) +c C) ↔ ∃a ∈ A ∃b ∈ B ∃c ∈ C ∃d(((a ∩ b) = ∅ ∧ d = (a ∪ b)) ∧ ((d ∩ c) = ∅ ∧ x = (d ∪ c))))
75		eladdc 4398	. . . 4 ⊢ (x ∈ (A +c (B +c C)) ↔ ∃a ∈ A ∃e ∈ (B +c C)((a ∩ e) = ∅ ∧ x = (a ∪ e)))
76		df-rex 2620	. . . . . 6 ⊢ (∃e ∈ (B +c C)((a ∩ e) = ∅ ∧ x = (a ∪ e)) ↔ ∃e(e ∈ (B +c C) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
77		rexcom4 2878	. . . . . . 7 ⊢ (∃b ∈ B ∃e∃c ∈ C (((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ ∃e∃b ∈ B ∃c ∈ C (((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
78		rexcom4 2878	. . . . . . . 8 ⊢ (∃c ∈ C ∃e(((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ ∃e∃c ∈ C (((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
79	78	rexbii 2639	. . . . . . 7 ⊢ (∃b ∈ B ∃c ∈ C ∃e(((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ ∃b ∈ B ∃e∃c ∈ C (((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
80		r19.41v 2764	. . . . . . . . 9 ⊢ (∃b ∈ B (∃c ∈ C ((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ (∃b ∈ B ∃c ∈ C ((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
81		r19.41v 2764	. . . . . . . . . 10 ⊢ (∃c ∈ C (((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ (∃c ∈ C ((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
82	81	rexbii 2639	. . . . . . . . 9 ⊢ (∃b ∈ B ∃c ∈ C (((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ ∃b ∈ B (∃c ∈ C ((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
83		eladdc 4398	. . . . . . . . . 10 ⊢ (e ∈ (B +c C) ↔ ∃b ∈ B ∃c ∈ C ((b ∩ c) = ∅ ∧ e = (b ∪ c)))
84	83	anbi1i 676	. . . . . . . . 9 ⊢ ((e ∈ (B +c C) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ (∃b ∈ B ∃c ∈ C ((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
85	80, 82, 84	3bitr4ri 269	. . . . . . . 8 ⊢ ((e ∈ (B +c C) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ ∃b ∈ B ∃c ∈ C (((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
86	85	exbii 1582	. . . . . . 7 ⊢ (∃e(e ∈ (B +c C) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ ∃e∃b ∈ B ∃c ∈ C (((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
87	77, 79, 86	3bitr4ri 269	. . . . . 6 ⊢ (∃e(e ∈ (B +c C) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))) ↔ ∃b ∈ B ∃c ∈ C ∃e(((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
88	76, 87	bitri 240	. . . . 5 ⊢ (∃e ∈ (B +c C)((a ∩ e) = ∅ ∧ x = (a ∪ e)) ↔ ∃b ∈ B ∃c ∈ C ∃e(((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
89	88	rexbii 2639	. . . 4 ⊢ (∃a ∈ A ∃e ∈ (B +c C)((a ∩ e) = ∅ ∧ x = (a ∪ e)) ↔ ∃a ∈ A ∃b ∈ B ∃c ∈ C ∃e(((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
90	75, 89	bitri 240	. . 3 ⊢ (x ∈ (A +c (B +c C)) ↔ ∃a ∈ A ∃b ∈ B ∃c ∈ C ∃e(((b ∩ c) = ∅ ∧ e = (b ∪ c)) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
91	53, 74, 90	3bitr4i 268	. 2 ⊢ (x ∈ ((A +c B) +c C) ↔ x ∈ (A +c (B +c C)))
92	91	eqriv 2350	1 ⊢ ((A +c B) +c C) = (A +c (B +c C))

Syntax hints:   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2615   ∪ cun 3207   ∩ cin 3208  ∅c0 3550   +_c cplc 4375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ral 2619  df-rex 2620  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-addc 4378

This theorem is referenced by:  addc32  4416  addc4  4417  addc6  4418  nncaddccl  4419  ltfinirr  4457  leltfintr  4458  ltfintr  4459  lefinlteq  4463  ltlefin  4468  sucoddeven  4511  evenodddisj  4516  sfinltfin  4535  lectr  6211  addceq0  6219  nclenn  6249  lecadd2  6266  ncslesuc  6267  nncdiv3  6277  nnc3n3p1  6278  nnc3n3p2  6279  nnc3p1n3p2  6280  nchoicelem1  6289  nchoicelem2  6290