Theorem xpassen 7649

Description: Associative law for equinumerosity of Cartesian product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by NM, 22-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)

Hypotheses

Ref	Expression
xpassen.1	|- A e. _V
xpassen.2	|- B e. _V
xpassen.3	|- C e. _V

Assertion

Ref	Expression
xpassen	|- ( ( A X. B ) X. C ) ~~ ( A X. ( B X. C ) )

Proof of Theorem xpassen

Dummy variables x y z w v u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpassen.1	. . . 4 |- A e. _V
2		xpassen.2	. . . 4 |- B e. _V
3	1, 2	xpex 6586	. . 3 |- ( A X. B ) e. _V
4		xpassen.3	. . 3 |- C e. _V
5	3, 4	xpex 6586	. 2 |- ( ( A X. B ) X. C ) e. _V
6	2, 4	xpex 6586	. . 3 |- ( B X. C ) e. _V
7	1, 6	xpex 6586	. 2 |- ( A X. ( B X. C ) ) e. _V
8		opex 4655	. . 3 |- <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. e. _V
9	8	a1i 11	. 2 |- ( x e. ( ( A X. B ) X. C ) -> <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. e. _V )
10		opex 4655	. . 3 |- <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. e. _V
11	10	a1i 11	. 2 |- ( y e. ( A X. ( B X. C ) ) -> <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. e. _V )
12		sneq 3982	. . . . . . . . . . . . . . . . 17 |- ( x = <. <. z , w >. , v >. -> { x } = { <. <. z , w >. , v >. } )
13	12	dmeqd 5026	. . . . . . . . . . . . . . . 16 |- ( x = <. <. z , w >. , v >. -> dom { x } = dom { <. <. z , w >. , v >. } )
14	13	unieqd 4201	. . . . . . . . . . . . . . 15 |- ( x = <. <. z , w >. , v >. -> U. dom { x } = U. dom { <. <. z , w >. , v >. } )
15	14	sneqd 3984	. . . . . . . . . . . . . 14 |- ( x = <. <. z , w >. , v >. -> { U. dom { x } } = { U. dom { <. <. z , w >. , v >. } } )
16	15	dmeqd 5026	. . . . . . . . . . . . 13 |- ( x = <. <. z , w >. , v >. -> dom { U. dom { x } } = dom { U. dom { <. <. z , w >. , v >. } } )
17	16	unieqd 4201	. . . . . . . . . . . 12 |- ( x = <. <. z , w >. , v >. -> U. dom { U. dom { x } } = U. dom { U. dom { <. <. z , w >. , v >. } } )
18		opex 4655	. . . . . . . . . . . . . . . . 17 |- <. z , w >. e. _V
19		vex 3062	. . . . . . . . . . . . . . . . 17 |- v e. _V
20	18, 19	op1sta 5306	. . . . . . . . . . . . . . . 16 |- U. dom { <. <. z , w >. , v >. } = <. z , w >.
21	20	sneqi 3983	. . . . . . . . . . . . . . 15 |- { U. dom { <. <. z , w >. , v >. } } = { <. z , w >. }
22	21	dmeqi 5025	. . . . . . . . . . . . . 14 |- dom { U. dom { <. <. z , w >. , v >. } } = dom { <. z , w >. }
23	22	unieqi 4200	. . . . . . . . . . . . 13 |- U. dom { U. dom { <. <. z , w >. , v >. } } = U. dom { <. z , w >. }
24		vex 3062	. . . . . . . . . . . . . 14 |- z e. _V
25		vex 3062	. . . . . . . . . . . . . 14 |- w e. _V
26	24, 25	op1sta 5306	. . . . . . . . . . . . 13 |- U. dom { <. z , w >. } = z
27	23, 26	eqtri 2431	. . . . . . . . . . . 12 |- U. dom { U. dom { <. <. z , w >. , v >. } } = z
28	17, 27	syl6req 2460	. . . . . . . . . . 11 |- ( x = <. <. z , w >. , v >. -> z = U. dom { U. dom { x } } )
29	15	rneqd 5051	. . . . . . . . . . . . . 14 |- ( x = <. <. z , w >. , v >. -> ran { U. dom { x } } = ran { U. dom { <. <. z , w >. , v >. } } )
30	29	unieqd 4201	. . . . . . . . . . . . 13 |- ( x = <. <. z , w >. , v >. -> U. ran { U. dom { x } } = U. ran { U. dom { <. <. z , w >. , v >. } } )
31	21	rneqi 5050	. . . . . . . . . . . . . . 15 |- ran { U. dom { <. <. z , w >. , v >. } } = ran { <. z , w >. }
32	31	unieqi 4200	. . . . . . . . . . . . . 14 |- U. ran { U. dom { <. <. z , w >. , v >. } } = U. ran { <. z , w >. }
33	24, 25	op2nda 5309	. . . . . . . . . . . . . 14 |- U. ran { <. z , w >. } = w
34	32, 33	eqtri 2431	. . . . . . . . . . . . 13 |- U. ran { U. dom { <. <. z , w >. , v >. } } = w
35	30, 34	syl6req 2460	. . . . . . . . . . . 12 |- ( x = <. <. z , w >. , v >. -> w = U. ran { U. dom { x } } )
36	12	rneqd 5051	. . . . . . . . . . . . . 14 |- ( x = <. <. z , w >. , v >. -> ran { x } = ran { <. <. z , w >. , v >. } )
37	36	unieqd 4201	. . . . . . . . . . . . 13 |- ( x = <. <. z , w >. , v >. -> U. ran { x } = U. ran { <. <. z , w >. , v >. } )
38	18, 19	op2nda 5309	. . . . . . . . . . . . 13 |- U. ran { <. <. z , w >. , v >. } = v
39	37, 38	syl6req 2460	. . . . . . . . . . . 12 |- ( x = <. <. z , w >. , v >. -> v = U. ran { x } )
40	35, 39	opeq12d 4167	. . . . . . . . . . 11 |- ( x = <. <. z , w >. , v >. -> <. w , v >. = <. U. ran { U. dom { x } } , U. ran { x } >. )
41	28, 40	opeq12d 4167	. . . . . . . . . 10 |- ( x = <. <. z , w >. , v >. -> <. z , <. w , v >. >. = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. )
42		sneq 3982	. . . . . . . . . . . . . . 15 |- ( y = <. z , <. w , v >. >. -> { y } = { <. z , <. w , v >. >. } )
43	42	dmeqd 5026	. . . . . . . . . . . . . 14 |- ( y = <. z , <. w , v >. >. -> dom { y } = dom { <. z , <. w , v >. >. } )
44	43	unieqd 4201	. . . . . . . . . . . . 13 |- ( y = <. z , <. w , v >. >. -> U. dom { y } = U. dom { <. z , <. w , v >. >. } )
45		opex 4655	. . . . . . . . . . . . . 14 |- <. w , v >. e. _V
46	24, 45	op1sta 5306	. . . . . . . . . . . . 13 |- U. dom { <. z , <. w , v >. >. } = z
47	44, 46	syl6req 2460	. . . . . . . . . . . 12 |- ( y = <. z , <. w , v >. >. -> z = U. dom { y } )
48	42	rneqd 5051	. . . . . . . . . . . . . . . . 17 |- ( y = <. z , <. w , v >. >. -> ran { y } = ran { <. z , <. w , v >. >. } )
49	48	unieqd 4201	. . . . . . . . . . . . . . . 16 |- ( y = <. z , <. w , v >. >. -> U. ran { y } = U. ran { <. z , <. w , v >. >. } )
50	49	sneqd 3984	. . . . . . . . . . . . . . 15 |- ( y = <. z , <. w , v >. >. -> { U. ran { y } } = { U. ran { <. z , <. w , v >. >. } } )
51	50	dmeqd 5026	. . . . . . . . . . . . . 14 |- ( y = <. z , <. w , v >. >. -> dom { U. ran { y } } = dom { U. ran { <. z , <. w , v >. >. } } )
52	51	unieqd 4201	. . . . . . . . . . . . 13 |- ( y = <. z , <. w , v >. >. -> U. dom { U. ran { y } } = U. dom { U. ran { <. z , <. w , v >. >. } } )
53	24, 45	op2nda 5309	. . . . . . . . . . . . . . . . 17 |- U. ran { <. z , <. w , v >. >. } = <. w , v >.
54	53	sneqi 3983	. . . . . . . . . . . . . . . 16 |- { U. ran { <. z , <. w , v >. >. } } = { <. w , v >. }
55	54	dmeqi 5025	. . . . . . . . . . . . . . 15 |- dom { U. ran { <. z , <. w , v >. >. } } = dom { <. w , v >. }
56	55	unieqi 4200	. . . . . . . . . . . . . 14 |- U. dom { U. ran { <. z , <. w , v >. >. } } = U. dom { <. w , v >. }
57	25, 19	op1sta 5306	. . . . . . . . . . . . . 14 |- U. dom { <. w , v >. } = w
58	56, 57	eqtri 2431	. . . . . . . . . . . . 13 |- U. dom { U. ran { <. z , <. w , v >. >. } } = w
59	52, 58	syl6req 2460	. . . . . . . . . . . 12 |- ( y = <. z , <. w , v >. >. -> w = U. dom { U. ran { y } } )
60	47, 59	opeq12d 4167	. . . . . . . . . . 11 |- ( y = <. z , <. w , v >. >. -> <. z , w >. = <. U. dom { y } , U. dom { U. ran { y } } >. )
61	50	rneqd 5051	. . . . . . . . . . . . 13 |- ( y = <. z , <. w , v >. >. -> ran { U. ran { y } } = ran { U. ran { <. z , <. w , v >. >. } } )
62	61	unieqd 4201	. . . . . . . . . . . 12 |- ( y = <. z , <. w , v >. >. -> U. ran { U. ran { y } } = U. ran { U. ran { <. z , <. w , v >. >. } } )
63	54	rneqi 5050	. . . . . . . . . . . . . 14 |- ran { U. ran { <. z , <. w , v >. >. } } = ran { <. w , v >. }
64	63	unieqi 4200	. . . . . . . . . . . . 13 |- U. ran { U. ran { <. z , <. w , v >. >. } } = U. ran { <. w , v >. }
65	25, 19	op2nda 5309	. . . . . . . . . . . . 13 |- U. ran { <. w , v >. } = v
66	64, 65	eqtri 2431	. . . . . . . . . . . 12 |- U. ran { U. ran { <. z , <. w , v >. >. } } = v
67	62, 66	syl6req 2460	. . . . . . . . . . 11 |- ( y = <. z , <. w , v >. >. -> v = U. ran { U. ran { y } } )
68	60, 67	opeq12d 4167	. . . . . . . . . 10 |- ( y = <. z , <. w , v >. >. -> <. <. z , w >. , v >. = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. )
69	41, 68	eq2tri 2470	. . . . . . . . 9 |- ( ( x = <. <. z , w >. , v >. /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( y = <. z , <. w , v >. >. /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
70		anass 647	. . . . . . . . 9 |- ( ( ( z e. A /\ w e. B ) /\ v e. C ) <-> ( z e. A /\ ( w e. B /\ v e. C ) ) )
71	69, 70	anbi12i 695	. . . . . . . 8 |- ( ( ( x = <. <. z , w >. , v >. /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) <-> ( ( y = <. z , <. w , v >. >. /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
72		an32 799	. . . . . . . 8 |- ( ( ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( ( x = <. <. z , w >. , v >. /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
73		an32 799	. . . . . . . 8 |- ( ( ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) <-> ( ( y = <. z , <. w , v >. >. /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
74	71, 72, 73	3bitr4i 277	. . . . . . 7 |- ( ( ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
75	74	exbii 1688	. . . . . 6 |- ( E. v ( ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> E. v ( ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
76		19.41v 1795	. . . . . 6 |- ( E. v ( ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) )
77		19.41v 1795	. . . . . 6 |- ( E. v ( ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) <-> ( E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
78	75, 76, 77	3bitr3i 275	. . . . 5 |- ( ( E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
79	78	2exbii 1689	. . . 4 |- ( E. z E. w ( E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> E. z E. w ( E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
80		19.41vv 1796	. . . 4 |- ( E. z E. w ( E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) )
81		19.41vv 1796	. . . 4 |- ( E. z E. w ( E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) <-> ( E. z E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
82	79, 80, 81	3bitr3i 275	. . 3 |- ( ( E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( E. z E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
83		elxp 4840	. . . . 5 |- ( x e. ( ( A X. B ) X. C ) <-> E. u E. v ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) )
84		excom 1873	. . . . 5 |- ( E. u E. v ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) <-> E. v E. u ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) )
85		elxp 4840	. . . . . . . . 9 |- ( u e. ( A X. B ) <-> E. z E. w ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) )
86	85	anbi1i 693	. . . . . . . 8 |- ( ( u e. ( A X. B ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> ( E. z E. w ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) )
87		an12 798	. . . . . . . 8 |- ( ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) <-> ( u e. ( A X. B ) /\ ( x = <. u , v >. /\ v e. C ) ) )
88		19.41vv 1796	. . . . . . . 8 |- ( E. z E. w ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> ( E. z E. w ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) )
89	86, 87, 88	3bitr4i 277	. . . . . . 7 |- ( ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) <-> E. z E. w ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) )
90	89	2exbii 1689	. . . . . 6 |- ( E. v E. u ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) <-> E. v E. u E. z E. w ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) )
91		exrot4 1877	. . . . . 6 |- ( E. v E. u E. z E. w ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> E. z E. w E. v E. u ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) )
92		anass 647	. . . . . . . . 9 |- ( ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> ( u = <. z , w >. /\ ( ( z e. A /\ w e. B ) /\ ( x = <. u , v >. /\ v e. C ) ) ) )
93	92	exbii 1688	. . . . . . . 8 |- ( E. u ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> E. u ( u = <. z , w >. /\ ( ( z e. A /\ w e. B ) /\ ( x = <. u , v >. /\ v e. C ) ) ) )
94		opeq1 4159	. . . . . . . . . . . 12 |- ( u = <. z , w >. -> <. u , v >. = <. <. z , w >. , v >. )
95	94	eqeq2d 2416	. . . . . . . . . . 11 |- ( u = <. z , w >. -> ( x = <. u , v >. <-> x = <. <. z , w >. , v >. ) )
96	95	anbi1d 703	. . . . . . . . . 10 |- ( u = <. z , w >. -> ( ( x = <. u , v >. /\ v e. C ) <-> ( x = <. <. z , w >. , v >. /\ v e. C ) ) )
97	96	anbi2d 702	. . . . . . . . 9 |- ( u = <. z , w >. -> ( ( ( z e. A /\ w e. B ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> ( ( z e. A /\ w e. B ) /\ ( x = <. <. z , w >. , v >. /\ v e. C ) ) ) )
98	18, 97	ceqsexv 3096	. . . . . . . 8 |- ( E. u ( u = <. z , w >. /\ ( ( z e. A /\ w e. B ) /\ ( x = <. u , v >. /\ v e. C ) ) ) <-> ( ( z e. A /\ w e. B ) /\ ( x = <. <. z , w >. , v >. /\ v e. C ) ) )
99		an12 798	. . . . . . . 8 |- ( ( ( z e. A /\ w e. B ) /\ ( x = <. <. z , w >. , v >. /\ v e. C ) ) <-> ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
100	93, 98, 99	3bitri 271	. . . . . . 7 |- ( E. u ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
101	100	3exbii 1690	. . . . . 6 |- ( E. z E. w E. v E. u ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
102	90, 91, 101	3bitri 271	. . . . 5 |- ( E. v E. u ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) <-> E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
103	83, 84, 102	3bitri 271	. . . 4 |- ( x e. ( ( A X. B ) X. C ) <-> E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
104	103	anbi1i 693	. . 3 |- ( ( x e. ( ( A X. B ) X. C ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) )
105		elxp 4840	. . . . 5 |- ( y e. ( A X. ( B X. C ) ) <-> E. z E. u ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) )
106		elxp 4840	. . . . . . . . . 10 |- ( u e. ( B X. C ) <-> E. w E. v ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) )
107	106	anbi2i 692	. . . . . . . . 9 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ u e. ( B X. C ) ) <-> ( ( y = <. z , u >. /\ z e. A ) /\ E. w E. v ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) )
108		anass 647	. . . . . . . . 9 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ u e. ( B X. C ) ) <-> ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) )
109		19.42vv 1801	. . . . . . . . . 10 |- ( E. w E. v ( ( y = <. z , u >. /\ z e. A ) /\ ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) <-> ( ( y = <. z , u >. /\ z e. A ) /\ E. w E. v ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) )
110		an12 798	. . . . . . . . . . . 12 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) <-> ( u = <. w , v >. /\ ( ( y = <. z , u >. /\ z e. A ) /\ ( w e. B /\ v e. C ) ) ) )
111		anass 647	. . . . . . . . . . . . 13 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ ( w e. B /\ v e. C ) ) <-> ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
112	111	anbi2i 692	. . . . . . . . . . . 12 |- ( ( u = <. w , v >. /\ ( ( y = <. z , u >. /\ z e. A ) /\ ( w e. B /\ v e. C ) ) ) <-> ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
113	110, 112	bitri 249	. . . . . . . . . . 11 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) <-> ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
114	113	2exbii 1689	. . . . . . . . . 10 |- ( E. w E. v ( ( y = <. z , u >. /\ z e. A ) /\ ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) <-> E. w E. v ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
115	109, 114	bitr3i 251	. . . . . . . . 9 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ E. w E. v ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) <-> E. w E. v ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
116	107, 108, 115	3bitr3i 275	. . . . . . . 8 |- ( ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) <-> E. w E. v ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
117	116	exbii 1688	. . . . . . 7 |- ( E. u ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) <-> E. u E. w E. v ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
118		exrot3 1876	. . . . . . 7 |- ( E. u E. w E. v ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) <-> E. w E. v E. u ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
119		opeq2 4160	. . . . . . . . . . 11 |- ( u = <. w , v >. -> <. z , u >. = <. z , <. w , v >. >. )
120	119	eqeq2d 2416	. . . . . . . . . 10 |- ( u = <. w , v >. -> ( y = <. z , u >. <-> y = <. z , <. w , v >. >. ) )
121	120	anbi1d 703	. . . . . . . . 9 |- ( u = <. w , v >. -> ( ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) <-> ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
122	45, 121	ceqsexv 3096	. . . . . . . 8 |- ( E. u ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) <-> ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
123	122	2exbii 1689	. . . . . . 7 |- ( E. w E. v E. u ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) <-> E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
124	117, 118, 123	3bitri 271	. . . . . 6 |- ( E. u ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) <-> E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
125	124	exbii 1688	. . . . 5 |- ( E. z E. u ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) <-> E. z E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
126	105, 125	bitri 249	. . . 4 |- ( y e. ( A X. ( B X. C ) ) <-> E. z E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
127	126	anbi1i 693	. . 3 |- ( ( y e. ( A X. ( B X. C ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) <-> ( E. z E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
128	82, 104, 127	3bitr4i 277	. 2 |- ( ( x e. ( ( A X. B ) X. C ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( y e. ( A X. ( B X. C ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
129	5, 7, 9, 11, 128	en2i 7591	1 |- ( ( A X. B ) X. C ) ~~ ( A X. ( B X. C ) )

Syntax hints:   /\ wa 367   = wceq 1405   E.wex 1633   e. wcel 1842   _Vcvv 3059   {csn 3972   <.cop 3978   U.cuni 4191   class class class wbr 4395   X. cxp 4821   dom cdm 4823   ran crn 4824   ~~ cen 7551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-en 7555

This theorem is referenced by: (None)