Theorem xpassen 7601

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 6704	. . 3 |- ( A X. B ) e. _V
4		xpassen.3	. . 3 |- C e. _V
5	3, 4	xpex 6704	. 2 |- ( ( A X. B ) X. C ) e. _V
6	2, 4	xpex 6704	. . 3 |- ( B X. C ) e. _V
7	1, 6	xpex 6704	. 2 |- ( A X. ( B X. C ) ) e. _V
8		opex 4704	. . 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 4704	. . 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 4030	. . . . . . . . . . . . . . . . 17 |- ( x = <. <. z , w >. , v >. -> { x } = { <. <. z , w >. , v >. } )
13	12	dmeqd 5196	. . . . . . . . . . . . . . . 16 |- ( x = <. <. z , w >. , v >. -> dom { x } = dom { <. <. z , w >. , v >. } )
14	13	unieqd 4248	. . . . . . . . . . . . . . 15 |- ( x = <. <. z , w >. , v >. -> U. dom { x } = U. dom { <. <. z , w >. , v >. } )
15	14	sneqd 4032	. . . . . . . . . . . . . 14 |- ( x = <. <. z , w >. , v >. -> { U. dom { x } } = { U. dom { <. <. z , w >. , v >. } } )
16	15	dmeqd 5196	. . . . . . . . . . . . 13 |- ( x = <. <. z , w >. , v >. -> dom { U. dom { x } } = dom { U. dom { <. <. z , w >. , v >. } } )
17	16	unieqd 4248	. . . . . . . . . . . 12 |- ( x = <. <. z , w >. , v >. -> U. dom { U. dom { x } } = U. dom { U. dom { <. <. z , w >. , v >. } } )
18		opex 4704	. . . . . . . . . . . . . . . . 17 |- <. z , w >. e. _V
19		vex 3109	. . . . . . . . . . . . . . . . 17 |- v e. _V
20	18, 19	op1sta 5481	. . . . . . . . . . . . . . . 16 |- U. dom { <. <. z , w >. , v >. } = <. z , w >.
21	20	sneqi 4031	. . . . . . . . . . . . . . 15 |- { U. dom { <. <. z , w >. , v >. } } = { <. z , w >. }
22	21	dmeqi 5195	. . . . . . . . . . . . . 14 |- dom { U. dom { <. <. z , w >. , v >. } } = dom { <. z , w >. }
23	22	unieqi 4247	. . . . . . . . . . . . 13 |- U. dom { U. dom { <. <. z , w >. , v >. } } = U. dom { <. z , w >. }
24		vex 3109	. . . . . . . . . . . . . 14 |- z e. _V
25		vex 3109	. . . . . . . . . . . . . 14 |- w e. _V
26	24, 25	op1sta 5481	. . . . . . . . . . . . 13 |- U. dom { <. z , w >. } = z
27	23, 26	eqtri 2489	. . . . . . . . . . . 12 |- U. dom { U. dom { <. <. z , w >. , v >. } } = z
28	17, 27	syl6req 2518	. . . . . . . . . . 11 |- ( x = <. <. z , w >. , v >. -> z = U. dom { U. dom { x } } )
29	15	rneqd 5221	. . . . . . . . . . . . . 14 |- ( x = <. <. z , w >. , v >. -> ran { U. dom { x } } = ran { U. dom { <. <. z , w >. , v >. } } )
30	29	unieqd 4248	. . . . . . . . . . . . 13 |- ( x = <. <. z , w >. , v >. -> U. ran { U. dom { x } } = U. ran { U. dom { <. <. z , w >. , v >. } } )
31	21	rneqi 5220	. . . . . . . . . . . . . . 15 |- ran { U. dom { <. <. z , w >. , v >. } } = ran { <. z , w >. }
32	31	unieqi 4247	. . . . . . . . . . . . . 14 |- U. ran { U. dom { <. <. z , w >. , v >. } } = U. ran { <. z , w >. }
33	24, 25	op2nda 5484	. . . . . . . . . . . . . 14 |- U. ran { <. z , w >. } = w
34	32, 33	eqtri 2489	. . . . . . . . . . . . 13 |- U. ran { U. dom { <. <. z , w >. , v >. } } = w
35	30, 34	syl6req 2518	. . . . . . . . . . . 12 |- ( x = <. <. z , w >. , v >. -> w = U. ran { U. dom { x } } )
36	12	rneqd 5221	. . . . . . . . . . . . . 14 |- ( x = <. <. z , w >. , v >. -> ran { x } = ran { <. <. z , w >. , v >. } )
37	36	unieqd 4248	. . . . . . . . . . . . 13 |- ( x = <. <. z , w >. , v >. -> U. ran { x } = U. ran { <. <. z , w >. , v >. } )
38	18, 19	op2nda 5484	. . . . . . . . . . . . 13 |- U. ran { <. <. z , w >. , v >. } = v
39	37, 38	syl6req 2518	. . . . . . . . . . . 12 |- ( x = <. <. z , w >. , v >. -> v = U. ran { x } )
40	35, 39	opeq12d 4214	. . . . . . . . . . 11 |- ( x = <. <. z , w >. , v >. -> <. w , v >. = <. U. ran { U. dom { x } } , U. ran { x } >. )
41	28, 40	opeq12d 4214	. . . . . . . . . 10 |- ( x = <. <. z , w >. , v >. -> <. z , <. w , v >. >. = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. )
42		sneq 4030	. . . . . . . . . . . . . . 15 |- ( y = <. z , <. w , v >. >. -> { y } = { <. z , <. w , v >. >. } )
43	42	dmeqd 5196	. . . . . . . . . . . . . 14 |- ( y = <. z , <. w , v >. >. -> dom { y } = dom { <. z , <. w , v >. >. } )
44	43	unieqd 4248	. . . . . . . . . . . . 13 |- ( y = <. z , <. w , v >. >. -> U. dom { y } = U. dom { <. z , <. w , v >. >. } )
45		opex 4704	. . . . . . . . . . . . . 14 |- <. w , v >. e. _V
46	24, 45	op1sta 5481	. . . . . . . . . . . . 13 |- U. dom { <. z , <. w , v >. >. } = z
47	44, 46	syl6req 2518	. . . . . . . . . . . 12 |- ( y = <. z , <. w , v >. >. -> z = U. dom { y } )
48	42	rneqd 5221	. . . . . . . . . . . . . . . . 17 |- ( y = <. z , <. w , v >. >. -> ran { y } = ran { <. z , <. w , v >. >. } )
49	48	unieqd 4248	. . . . . . . . . . . . . . . 16 |- ( y = <. z , <. w , v >. >. -> U. ran { y } = U. ran { <. z , <. w , v >. >. } )
50	49	sneqd 4032	. . . . . . . . . . . . . . 15 |- ( y = <. z , <. w , v >. >. -> { U. ran { y } } = { U. ran { <. z , <. w , v >. >. } } )
51	50	dmeqd 5196	. . . . . . . . . . . . . 14 |- ( y = <. z , <. w , v >. >. -> dom { U. ran { y } } = dom { U. ran { <. z , <. w , v >. >. } } )
52	51	unieqd 4248	. . . . . . . . . . . . 13 |- ( y = <. z , <. w , v >. >. -> U. dom { U. ran { y } } = U. dom { U. ran { <. z , <. w , v >. >. } } )
53	24, 45	op2nda 5484	. . . . . . . . . . . . . . . . 17 |- U. ran { <. z , <. w , v >. >. } = <. w , v >.
54	53	sneqi 4031	. . . . . . . . . . . . . . . 16 |- { U. ran { <. z , <. w , v >. >. } } = { <. w , v >. }
55	54	dmeqi 5195	. . . . . . . . . . . . . . 15 |- dom { U. ran { <. z , <. w , v >. >. } } = dom { <. w , v >. }
56	55	unieqi 4247	. . . . . . . . . . . . . 14 |- U. dom { U. ran { <. z , <. w , v >. >. } } = U. dom { <. w , v >. }
57	25, 19	op1sta 5481	. . . . . . . . . . . . . 14 |- U. dom { <. w , v >. } = w
58	56, 57	eqtri 2489	. . . . . . . . . . . . 13 |- U. dom { U. ran { <. z , <. w , v >. >. } } = w
59	52, 58	syl6req 2518	. . . . . . . . . . . 12 |- ( y = <. z , <. w , v >. >. -> w = U. dom { U. ran { y } } )
60	47, 59	opeq12d 4214	. . . . . . . . . . 11 |- ( y = <. z , <. w , v >. >. -> <. z , w >. = <. U. dom { y } , U. dom { U. ran { y } } >. )
61	50	rneqd 5221	. . . . . . . . . . . . 13 |- ( y = <. z , <. w , v >. >. -> ran { U. ran { y } } = ran { U. ran { <. z , <. w , v >. >. } } )
62	61	unieqd 4248	. . . . . . . . . . . 12 |- ( y = <. z , <. w , v >. >. -> U. ran { U. ran { y } } = U. ran { U. ran { <. z , <. w , v >. >. } } )
63	54	rneqi 5220	. . . . . . . . . . . . . 14 |- ran { U. ran { <. z , <. w , v >. >. } } = ran { <. w , v >. }
64	63	unieqi 4247	. . . . . . . . . . . . 13 |- U. ran { U. ran { <. z , <. w , v >. >. } } = U. ran { <. w , v >. }
65	25, 19	op2nda 5484	. . . . . . . . . . . . 13 |- U. ran { <. w , v >. } = v
66	64, 65	eqtri 2489	. . . . . . . . . . . 12 |- U. ran { U. ran { <. z , <. w , v >. >. } } = v
67	62, 66	syl6req 2518	. . . . . . . . . . 11 |- ( y = <. z , <. w , v >. >. -> v = U. ran { U. ran { y } } )
68	60, 67	opeq12d 4214	. . . . . . . . . 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 2528	. . . . . . . . 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 649	. . . . . . . . 9 |- ( ( ( z e. A /\ w e. B ) /\ v e. C ) <-> ( z e. A /\ ( w e. B /\ v e. C ) ) )
71	69, 70	anbi12i 697	. . . . . . . 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 796	. . . . . . . 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 796	. . . . . . . 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 1639	. . . . . 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 1938	. . . . . 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 1938	. . . . . 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 1640	. . . 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 1939	. . . 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 1939	. . . 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 5009	. . . . 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 1793	. . . . 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 5009	. . . . . . . . 9 |- ( u e. ( A X. B ) <-> E. z E. w ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) )
86	85	anbi1i 695	. . . . . . . 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 795	. . . . . . . 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 1939	. . . . . . . 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 1640	. . . . . 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 1797	. . . . . 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 649	. . . . . . . . 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 1639	. . . . . . . 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 4206	. . . . . . . . . . . 12 |- ( u = <. z , w >. -> <. u , v >. = <. <. z , w >. , v >. )
95	94	eqeq2d 2474	. . . . . . . . . . 11 |- ( u = <. z , w >. -> ( x = <. u , v >. <-> x = <. <. z , w >. , v >. ) )
96	95	anbi1d 704	. . . . . . . . . 10 |- ( u = <. z , w >. -> ( ( x = <. u , v >. /\ v e. C ) <-> ( x = <. <. z , w >. , v >. /\ v e. C ) ) )
97	96	anbi2d 703	. . . . . . . . 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 3143	. . . . . . . 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 795	. . . . . . . 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 1641	. . . . . 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 695	. . 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 5009	. . . . 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 5009	. . . . . . . . . 10 |- ( u e. ( B X. C ) <-> E. w E. v ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) )
107	106	anbi2i 694	. . . . . . . . 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 649	. . . . . . . . 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 1944	. . . . . . . . . 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 795	. . . . . . . . . . . 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 649	. . . . . . . . . . . . 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 694	. . . . . . . . . . . 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 1640	. . . . . . . . . 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 1639	. . . . . . 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 1796	. . . . . . 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 4207	. . . . . . . . . . 11 |- ( u = <. w , v >. -> <. z , u >. = <. z , <. w , v >. >. )
120	119	eqeq2d 2474	. . . . . . . . . 10 |- ( u = <. w , v >. -> ( y = <. z , u >. <-> y = <. z , <. w , v >. >. ) )
121	120	anbi1d 704	. . . . . . . . 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 3143	. . . . . . . 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 1640	. . . . . . 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 1639	. . . . 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 695	. . 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 7543	1 |- ( ( A X. B ) X. C ) ~~ ( A X. ( B X. C ) )

Syntax hints:   /\ wa 369   = wceq 1374   E.wex 1591   e. wcel 1762   _Vcvv 3106   {csn 4020   <.cop 4026   U.cuni 4238   class class class wbr 4440   X. cxp 4990   dom cdm 4992   ran crn 4993   ~~ cen 7503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-en 7507

This theorem is referenced by: (None)