Theorem xpassen 4447

Description: Associative law for equinumerosity of cross product. Proposition 4.22(e) of [Mendelson] p. 254.

Hypotheses

Ref	Expression
xpassen.1	⊢ A ∈ V
xpassen.2	⊢ B ∈ V
xpassen.3	⊢ C ∈ V

Assertion

Ref	Expression
xpassen	⊢ ((A × B) × C) ≈ (A × (B × C))

Proof of Theorem xpassen

Step	Hyp	Ref	Expression
1		xpassen.1	. . . 4 ⊢ A ∈ V
2		xpassen.2	. . . 4 ⊢ B ∈ V
3	1, 2	xpex 3266	. . 3 ⊢ (A × B) ∈ V
4		xpassen.3	. . 3 ⊢ C ∈ V
5	3, 4	xpex 3266	. 2 ⊢ ((A × B) × C) ∈ V
6		opex 2788	. . 3 ⊢ ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩ ∈ V
7	6	a1i 8	. 2 ⊢ (x ∈ ((A × B) × C) → ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩ ∈ V)
8		opex 2788	. . 3 ⊢ ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩ ∈ V
9	8	a1i 8	. 2 ⊢ (y ∈ (A × (B × C)) → ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩ ∈ V)
10		sneq 2421	. . . . . . . . . . . . . . . . 17 ⊢ (x = ⟨⟨z, w⟩, v⟩ → {x} = {⟨⟨z, w⟩, v⟩})
11	10	dmeqd 3319	. . . . . . . . . . . . . . . 16 ⊢ (x = ⟨⟨z, w⟩, v⟩ → dom { x} = dom {⟨⟨z, w⟩, v⟩})
12	11	unieqd 2516	. . . . . . . . . . . . . . 15 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ∪dom { x} = ∪dom {⟨⟨z, w⟩, v⟩})
13	12	sneqd 2423	. . . . . . . . . . . . . 14 ⊢ (x = ⟨⟨z, w⟩, v⟩ → {∪dom { x}} = {∪dom {⟨⟨z, w⟩, v⟩}})
14	13	dmeqd 3319	. . . . . . . . . . . . 13 ⊢ (x = ⟨⟨z, w⟩, v⟩ → dom {∪dom { x}} = dom {∪dom {⟨⟨z, w⟩, v⟩}})
15	14	unieqd 2516	. . . . . . . . . . . 12 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ∪dom {∪dom { x}} = ∪dom {∪dom {⟨⟨z, w⟩, v⟩}})
16		opex 2788	. . . . . . . . . . . . . . . . 17 ⊢ ⟨z, w⟩ ∈ V
17	16	op1sta 3454	. . . . . . . . . . . . . . . 16 ⊢ ∪dom {⟨⟨z, w⟩, v⟩} = ⟨z, w⟩
18	17	sneqi 2422	. . . . . . . . . . . . . . 15 ⊢ {∪dom {⟨⟨z, w⟩, v⟩}} = {⟨z, w⟩}
19	18	dmeqi 3318	. . . . . . . . . . . . . 14 ⊢ dom {∪dom {⟨⟨z, w⟩, v⟩}} = dom {⟨z, w⟩}
20	19	unieqi 2515	. . . . . . . . . . . . 13 ⊢ ∪dom {∪dom {⟨⟨z, w⟩, v⟩}} = ∪dom {⟨z, w⟩}
21		visset 1816	. . . . . . . . . . . . . 14 ⊢ z ∈ V
22	21	op1sta 3454	. . . . . . . . . . . . 13 ⊢ ∪dom {⟨z, w⟩} = z
23	20, 22	eqtr 1498	. . . . . . . . . . . 12 ⊢ ∪dom {∪dom {⟨⟨z, w⟩, v⟩}} = z
24	15, 23	syl6req 1527	. . . . . . . . . . 11 ⊢ (x = ⟨⟨z, w⟩, v⟩ → z = ∪dom {∪dom { x}})
25	13	rneqd 3347	. . . . . . . . . . . . . 14 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ran {∪dom { x}} = ran {∪dom {⟨⟨z, w⟩, v⟩}})
26	25	unieqd 2516	. . . . . . . . . . . . 13 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ∪ran {∪dom { x}} = ∪ran {∪dom {⟨⟨z, w⟩, v⟩}})
27	18	rneqi 3346	. . . . . . . . . . . . . . 15 ⊢ ran {∪dom {⟨⟨z, w⟩, v⟩}} = ran {⟨z, w⟩}
28	27	unieqi 2515	. . . . . . . . . . . . . 14 ⊢ ∪ran {∪dom {⟨⟨z, w⟩, v⟩}} = ∪ran {⟨z, w⟩}
29		visset 1816	. . . . . . . . . . . . . . 15 ⊢ w ∈ V
30	21, 29	op2nda 3458	. . . . . . . . . . . . . 14 ⊢ ∪ran {⟨z, w⟩} = w
31	28, 30	eqtr 1498	. . . . . . . . . . . . 13 ⊢ ∪ran {∪dom {⟨⟨z, w⟩, v⟩}} = w
32	26, 31	syl6req 1527	. . . . . . . . . . . 12 ⊢ (x = ⟨⟨z, w⟩, v⟩ → w = ∪ran {∪dom { x}})
33	10	rneqd 3347	. . . . . . . . . . . . . 14 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ran { x} = ran {⟨⟨z, w⟩, v⟩})
34	33	unieqd 2516	. . . . . . . . . . . . 13 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ∪ran { x} = ∪ran {⟨⟨z, w⟩, v⟩})
35		visset 1816	. . . . . . . . . . . . . 14 ⊢ v ∈ V
36	16, 35	op2nda 3458	. . . . . . . . . . . . 13 ⊢ ∪ran {⟨⟨z, w⟩, v⟩} = v
37	34, 36	syl6req 1527	. . . . . . . . . . . 12 ⊢ (x = ⟨⟨z, w⟩, v⟩ → v = ∪ran { x})
38	32, 37	opeq12d 2499	. . . . . . . . . . 11 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ⟨w, v⟩ = ⟨∪ran {∪dom { x}}, ∪ran { x}⟩)
39	24, 38	opeq12d 2499	. . . . . . . . . 10 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ⟨z, ⟨w, v⟩⟩ = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩)
40		sneq 2421	. . . . . . . . . . . . . . 15 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → {y} = {⟨z, ⟨w, v⟩⟩})
41	40	dmeqd 3319	. . . . . . . . . . . . . 14 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → dom { y} = dom {⟨z, ⟨w, v⟩⟩})
42	41	unieqd 2516	. . . . . . . . . . . . 13 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ∪dom { y} = ∪dom {⟨z, ⟨w, v⟩⟩})
43	21	op1sta 3454	. . . . . . . . . . . . 13 ⊢ ∪dom {⟨z, ⟨w, v⟩⟩} = z
44	42, 43	syl6req 1527	. . . . . . . . . . . 12 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → z = ∪dom { y})
45	40	rneqd 3347	. . . . . . . . . . . . . . . . 17 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ran { y} = ran {⟨z, ⟨w, v⟩⟩})
46	45	unieqd 2516	. . . . . . . . . . . . . . . 16 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ∪ran { y} = ∪ran {⟨z, ⟨w, v⟩⟩})
47	46	sneqd 2423	. . . . . . . . . . . . . . 15 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → {∪ran { y}} = {∪ran {⟨z, ⟨w, v⟩⟩}})
48	47	dmeqd 3319	. . . . . . . . . . . . . 14 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → dom {∪ran { y}} = dom {∪ran {⟨z, ⟨w, v⟩⟩}})
49	48	unieqd 2516	. . . . . . . . . . . . 13 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ∪dom {∪ran { y}} = ∪dom {∪ran {⟨z, ⟨w, v⟩⟩}})
50		opex 2788	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨w, v⟩ ∈ V
51	21, 50	op2nda 3458	. . . . . . . . . . . . . . . . 17 ⊢ ∪ran {⟨z, ⟨w, v⟩⟩} = ⟨w, v⟩
52	51	sneqi 2422	. . . . . . . . . . . . . . . 16 ⊢ {∪ran {⟨z, ⟨w, v⟩⟩}} = {⟨w, v⟩}
53	52	dmeqi 3318	. . . . . . . . . . . . . . 15 ⊢ dom {∪ran {⟨z, ⟨w, v⟩⟩}} = dom {⟨w, v⟩}
54	53	unieqi 2515	. . . . . . . . . . . . . 14 ⊢ ∪dom {∪ran {⟨z, ⟨w, v⟩⟩}} = ∪dom {⟨w, v⟩}
55	29	op1sta 3454	. . . . . . . . . . . . . 14 ⊢ ∪dom {⟨w, v⟩} = w
56	54, 55	eqtr 1498	. . . . . . . . . . . . 13 ⊢ ∪dom {∪ran {⟨z, ⟨w, v⟩⟩}} = w
57	49, 56	syl6req 1527	. . . . . . . . . . . 12 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → w = ∪dom {∪ran { y}})
58	44, 57	opeq12d 2499	. . . . . . . . . . 11 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ⟨z, w⟩ = ⟨∪dom { y}, ∪dom {∪ran { y}}⟩)
59	47	rneqd 3347	. . . . . . . . . . . . 13 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ran {∪ran { y}} = ran {∪ran {⟨z, ⟨w, v⟩⟩}})
60	59	unieqd 2516	. . . . . . . . . . . 12 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ∪ran {∪ran { y}} = ∪ran {∪ran {⟨z, ⟨w, v⟩⟩}})
61	52	rneqi 3346	. . . . . . . . . . . . . 14 ⊢ ran {∪ran {⟨z, ⟨w, v⟩⟩}} = ran {⟨w, v⟩}
62	61	unieqi 2515	. . . . . . . . . . . . 13 ⊢ ∪ran {∪ran {⟨z, ⟨w, v⟩⟩}} = ∪ran {⟨w, v⟩}
63	29, 35	op2nda 3458	. . . . . . . . . . . . 13 ⊢ ∪ran {⟨w, v⟩} = v
64	62, 63	eqtr 1498	. . . . . . . . . . . 12 ⊢ ∪ran {∪ran {⟨z, ⟨w, v⟩⟩}} = v
65	60, 64	syl6req 1527	. . . . . . . . . . 11 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → v = ∪ran {∪ran { y}})
66	58, 65	opeq12d 2499	. . . . . . . . . 10 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ⟨⟨z, w⟩, v⟩ = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩)
67	39, 66	eq2tr 1536	. . . . . . . . 9 ⊢ ((x = ⟨⟨z, w⟩, v⟩ ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩) ↔ (y = ⟨z, ⟨w, v⟩⟩ ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩))
68		anass 441	. . . . . . . . 9 ⊢ (((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C) ↔ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C)))
69	67, 68	anbi12i 484	. . . . . . . 8 ⊢ (((x = ⟨⟨z, w⟩, v⟩ ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩) ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)) ↔ ((y = ⟨z, ⟨w, v⟩⟩ ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩) ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))))
70		an23 487	. . . . . . . 8 ⊢ (((x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)) ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩) ↔ ((x = ⟨⟨z, w⟩, v⟩ ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩) ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)))
71		an23 487	. . . . . . . 8 ⊢ (((y = ⟨z, ⟨w, v⟩⟩ ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))) ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩) ↔ ((y = ⟨z, ⟨w, v⟩⟩ ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩) ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))))
72	69, 70, 71	3bitr4 183	. . . . . . 7 ⊢ (((x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)) ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩) ↔ ((y = ⟨z, ⟨w, v⟩⟩ ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))) ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩))
73	72	exbii 1053	. . . . . 6 ⊢ (∃v((x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)) ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩) ↔ ∃v((y = ⟨z, ⟨w, v⟩⟩ ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))) ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩))
74		19.41v 1307	. . . . . 6 ⊢ (∃v((x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)) ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩) ↔ (∃v(x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)) ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩))
75		19.41v 1307	. . . . . 6 ⊢ (∃v((y = ⟨z, ⟨w, v⟩⟩ ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))) ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩) ↔ (∃v(y = ⟨z, ⟨w, v⟩⟩ ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))) ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩))
76	73, 74, 75	3bitr3 181	. . . . 5 ⊢ ((∃v(x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)) ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩) ↔ (∃v(y = ⟨z, ⟨w, v⟩⟩ ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))) ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩))
77	76	2exbii 1054	. . . 4 ⊢ (∃z∃w(∃v(x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)) ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩) ↔ ∃z∃w(∃v(y = ⟨z, ⟨w, v⟩⟩ ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))) ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩))
78		19.41vv 1308	. . . 4 ⊢ (∃z∃w(∃v(x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)) ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩) ↔ (∃z∃w∃v(x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)) ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩))
79		19.41vv 1308	. . . 4 ⊢ (∃z∃w(∃v(y = ⟨z, ⟨w, v⟩⟩ ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))) ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩) ↔ (∃z∃w∃v(y = ⟨z, ⟨w, v⟩⟩ ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))) ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩))
80	77, 78, 79	3bitr3 181	. . 3 ⊢ ((∃z∃w∃v(x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)) ⋀ y = ⟨∪dom {∪dom { x}}, ⟨∪ran {∪dom { x}}, ∪ran { x}⟩⟩) ↔ (∃z∃w∃v(y = ⟨z, ⟨w, v⟩⟩ ⋀ (z ∈ A ⋀ (w ∈ B ⋀ v ∈ C))) ⋀ x = ⟨⟨∪dom { y}, ∪dom {∪ran { y}}⟩, ∪ran {∪ran { y}}⟩))
81		elxp 3208	. . . . 5 ⊢ (x ∈ ((A × B) × C) ↔ ∃u∃v(x = ⟨u, v⟩ ⋀ (u ∈ (A × B) ⋀ v ∈ C)))
82		excom 1048	. . . . 5 ⊢ (∃u∃v(x = ⟨u, v⟩ ⋀ (u ∈ (A × B) ⋀ v ∈ C)) ↔ ∃v∃u(x = ⟨u, v⟩ ⋀ (u ∈ (A × B) ⋀ v ∈ C)))
83		elxp 3208	. . . . . . . . 9 ⊢ (u ∈ (A × B) ↔ ∃z∃w(u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)))
84	83	anbi1i 483	. . . . . . . 8 ⊢ ((u ∈ (A × B) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)) ↔ (∃z∃w(u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)))
85		an12 486	. . . . . . . 8 ⊢ ((x = ⟨u, v⟩ ⋀ (u ∈ (A × B) ⋀ v ∈ C)) ↔ (u ∈ (A × B) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)))
86		19.41vv 1308	. . . . . . . 8 ⊢ (∃z∃w((u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)) ↔ (∃z∃w(u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)))
87	84, 85, 86	3bitr4 183	. . . . . . 7 ⊢ ((x = ⟨u, v⟩ ⋀ (u ∈ (A × B) ⋀ v ∈ C)) ↔ ∃z∃w((u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)))
88	87	2exbii 1054	. . . . . 6 ⊢ (∃v∃u(x = ⟨u, v⟩ ⋀ (u ∈ (A × B) ⋀ v ∈ C)) ↔ ∃v∃u∃z∃w((u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)))
89		exrot4 1102	. . . . . 6 ⊢ (∃v∃u∃z∃w((u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)) ↔ ∃z∃w∃v∃u((u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)))
90		anass 441	. . . . . . . . 9 ⊢ (((u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)) ↔ (u = ⟨z, w⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C))))
91	90	exbii 1053	. . . . . . . 8 ⊢ (∃u((u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)) ↔ ∃u(u = ⟨z, w⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C))))
92		opeq1 2491	. . . . . . . . . . . 12 ⊢ (u = ⟨z, w⟩ → ⟨u, v⟩ = ⟨⟨z, w⟩, v⟩)
93	92	eqeq2d 1489	. . . . . . . . . . 11 ⊢ (u = ⟨z, w⟩ → (x = ⟨u, v⟩ ↔ x = ⟨⟨z, w⟩, v⟩))
94	93	anbi1d 619	. . . . . . . . . 10 ⊢ (u = ⟨z, w⟩ → ((x = ⟨u, v⟩ ⋀ v ∈ C) ↔ (x = ⟨⟨z, w⟩, v⟩ ⋀ v ∈ C)))
95	94	anbi2d 618	. . . . . . . . 9 ⊢ (u = ⟨z, w⟩ → (((z ∈ A ⋀ w ∈ B) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)) ↔ ((z ∈ A ⋀ w ∈ B) ⋀ (x = ⟨⟨z, w⟩, v⟩ ⋀ v ∈ C))))
96	16, 95	ceqsexv 1838	. . . . . . . 8 ⊢ (∃u(u = ⟨z, w⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C))) ↔ ((z ∈ A ⋀ w ∈ B) ⋀ (x = ⟨⟨z, w⟩, v⟩ ⋀ v ∈ C)))
97		an12 486	. . . . . . . 8 ⊢ (((z ∈ A ⋀ w ∈ B) ⋀ (x = ⟨⟨z, w⟩, v⟩ ⋀ v ∈ C)) ↔ (x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)))
98	91, 96, 97	3bitr 177	. . . . . . 7 ⊢ (∃u((u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)) ↔ (x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)))
99	98	3exbi 1055	. . . . . 6 ⊢ (∃z∃w∃v∃u((u = ⟨z, w⟩ ⋀ (z ∈ A ⋀ w ∈ B)) ⋀ (x = ⟨u, v⟩ ⋀ v ∈ C)) ↔ ∃z∃w∃v(x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)))
100	88, 89, 99	3bitr 177	. . . . 5 ⊢ (∃v∃u(x = ⟨u, v⟩ ⋀ (u ∈ (A × B) ⋀ v ∈ C)) ↔ ∃z∃w∃v(x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w ∈ B) ⋀ v ∈ C)))
101	81, 82, 100	3bitr 177	. . . 4 ⊢ (x ∈ ((A × B) × C) ↔ ∃z∃w∃v(x = ⟨⟨z, w⟩, v⟩ ⋀ ((z ∈ A ⋀ w &isin