Theorem addcass 4416

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 3504	. . . . . . . . . . . 12 ⊢ ((a ∪ b) ∩ c) = ((a ∩ c) ∪ (b ∩ c))
6	5	eqeq1i 2360	. . . . . . . . . . 11 ⊢ (((a ∪ b) ∩ c) = ∅ ↔ ((a ∩ c) ∪ (b ∩ c)) = ∅)
7		un00 3587	. . . . . . . . . . 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 3502	. . . . . . . . . . . 12 ⊢ (a ∩ (b ∪ c)) = ((a ∩ b) ∪ (a ∩ c))
11	10	eqeq1i 2360	. . . . . . . . . . 11 ⊢ ((a ∩ (b ∪ c)) = ∅ ↔ ((a ∩ b) ∪ (a ∩ c)) = ∅)
12		un00 3587	. . . . . . . . . . 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 3421	. . . . . . . . 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 2863	. . . . . . . . 9 ⊢ a ∈ V
27		vex 2863	. . . . . . . . 9 ⊢ b ∈ V
28	26, 27	unex 4107	. . . . . . . 8 ⊢ (a ∪ b) ∈ V
29		ineq1 3451	. . . . . . . . . . 11 ⊢ (d = (a ∪ b) → (d ∩ c) = ((a ∪ b) ∩ c))
30	29	eqeq1d 2361	. . . . . . . . . 10 ⊢ (d = (a ∪ b) → ((d ∩ c) = ∅ ↔ ((a ∪ b) ∩ c) = ∅))
31		uneq1 3412	. . . . . . . . . . 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 2895	. . . . . . 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 2863	. . . . . . . . 9 ⊢ c ∈ V
42	27, 41	unex 4107	. . . . . . . 8 ⊢ (b ∪ c) ∈ V
43		ineq2 3452	. . . . . . . . . . 11 ⊢ (e = (b ∪ c) → (a ∩ e) = (a ∩ (b ∪ c)))
44	43	eqeq1d 2361	. . . . . . . . . 10 ⊢ (e = (b ∪ c) → ((a ∩ e) = ∅ ↔ (a ∩ (b ∪ c)) = ∅))
45		uneq2 3413	. . . . . . . . . . 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 2895	. . . . . . 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 2640	. . . 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 2642	. . 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 4399	. . . 4 ⊢ (x ∈ ((A +c B) +c C) ↔ ∃d ∈ (A +c B)∃c ∈ C ((d ∩ c) = ∅ ∧ x = (d ∪ c)))
55		df-rex 2621	. . . . 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 2879	. . . . . 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 2879	. . . . . . . . . 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 2766	. . . . . . . . . . 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 2640	. . . . . . . 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 2879	. . . . . . . 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 2640	. . . . . 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 2765	. . . . . . . 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 2765	. . . . . . . . 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 2640	. . . . . . . 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 4399	. . . . . . . . 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 4399	. . . 4 ⊢ (x ∈ (A +c (B +c C)) ↔ ∃a ∈ A ∃e ∈ (B +c C)((a ∩ e) = ∅ ∧ x = (a ∪ e)))
76		df-rex 2621	. . . . . 6 ⊢ (∃e ∈ (B +c C)((a ∩ e) = ∅ ∧ x = (a ∪ e)) ↔ ∃e(e ∈ (B +c C) ∧ ((a ∩ e) = ∅ ∧ x = (a ∪ e))))
77		rexcom4 2879	. . . . . . 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 2879	. . . . . . . 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 2640	. . . . . . 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 2765	. . . . . . . . 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 2765	. . . . . . . . . 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 2640	. . . . . . . . 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 4399	. . . . . . . . . 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 2640	. . . 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 2616   ∪ cun 3208   ∩ cin 3209  ∅c0 3551   +_c cplc 4376

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 4079

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 2479  df-ral 2620  df-rex 2621  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-ss 3260  df-nul 3552  df-addc 4379

This theorem is referenced by:  addc32  4417  addc4  4418  addc6  4419  nncaddccl  4420  ltfinirr  4458  leltfintr  4459  ltfintr  4460  lefinlteq  4464  ltlefin  4469  sucoddeven  4512  evenodddisj  4517  sfinltfin  4536  lectr  6212  addceq0  6220  nclenn  6250  lecadd2  6267  ncslesuc  6268  nncdiv3  6278  nnc3n3p1  6279  nnc3n3p2  6280  nnc3p1n3p2  6281  nchoicelem1  6290  nchoicelem2  6291