Theorem xpassen 7631

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
xpassen.2
xpassen.3

Assertion

Ref	Expression
xpassen

Proof of Theorem xpassen

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpassen.1	. . . 4
2		xpassen.2	. . . 4
3	1, 2	xpex 6604	. . 3
4		xpassen.3	. . 3
5	3, 4	xpex 6604	. 2
6	2, 4	xpex 6604	. . 3
7	1, 6	xpex 6604	. 2
8		opex 4716	. . 3
9	8	a1i 11	. 2
10		opex 4716	. . 3
11	10	a1i 11	. 2
12		sneq 4039	. . . . . . . . . . . . . . . . 17
13	12	dmeqd 5210	. . . . . . . . . . . . . . . 16
14	13	unieqd 4259	. . . . . . . . . . . . . . 15
15	14	sneqd 4041	. . . . . . . . . . . . . 14
16	15	dmeqd 5210	. . . . . . . . . . . . 13
17	16	unieqd 4259	. . . . . . . . . . . 12
18		opex 4716	. . . . . . . . . . . . . . . . 17
19		vex 3112	. . . . . . . . . . . . . . . . 17
20	18, 19	op1sta 5495	. . . . . . . . . . . . . . . 16
21	20	sneqi 4040	. . . . . . . . . . . . . . 15
22	21	dmeqi 5209	. . . . . . . . . . . . . 14
23	22	unieqi 4258	. . . . . . . . . . . . 13
24		vex 3112	. . . . . . . . . . . . . 14
25		vex 3112	. . . . . . . . . . . . . 14
26	24, 25	op1sta 5495	. . . . . . . . . . . . 13
27	23, 26	eqtri 2486	. . . . . . . . . . . 12
28	17, 27	syl6req 2515	. . . . . . . . . . 11
29	15	rneqd 5235	. . . . . . . . . . . . . 14
30	29	unieqd 4259	. . . . . . . . . . . . 13
31	21	rneqi 5234	. . . . . . . . . . . . . . 15
32	31	unieqi 4258	. . . . . . . . . . . . . 14
33	24, 25	op2nda 5498	. . . . . . . . . . . . . 14
34	32, 33	eqtri 2486	. . . . . . . . . . . . 13
35	30, 34	syl6req 2515	. . . . . . . . . . . 12
36	12	rneqd 5235	. . . . . . . . . . . . . 14
37	36	unieqd 4259	. . . . . . . . . . . . 13
38	18, 19	op2nda 5498	. . . . . . . . . . . . 13
39	37, 38	syl6req 2515	. . . . . . . . . . . 12
40	35, 39	opeq12d 4225	. . . . . . . . . . 11
41	28, 40	opeq12d 4225	. . . . . . . . . 10
42		sneq 4039	. . . . . . . . . . . . . . 15
43	42	dmeqd 5210	. . . . . . . . . . . . . 14
44	43	unieqd 4259	. . . . . . . . . . . . 13
45		opex 4716	. . . . . . . . . . . . . 14
46	24, 45	op1sta 5495	. . . . . . . . . . . . 13
47	44, 46	syl6req 2515	. . . . . . . . . . . 12
48	42	rneqd 5235	. . . . . . . . . . . . . . . . 17
49	48	unieqd 4259	. . . . . . . . . . . . . . . 16
50	49	sneqd 4041	. . . . . . . . . . . . . . 15
51	50	dmeqd 5210	. . . . . . . . . . . . . 14
52	51	unieqd 4259	. . . . . . . . . . . . 13
53	24, 45	op2nda 5498	. . . . . . . . . . . . . . . . 17
54	53	sneqi 4040	. . . . . . . . . . . . . . . 16
55	54	dmeqi 5209	. . . . . . . . . . . . . . 15
56	55	unieqi 4258	. . . . . . . . . . . . . 14
57	25, 19	op1sta 5495	. . . . . . . . . . . . . 14
58	56, 57	eqtri 2486	. . . . . . . . . . . . 13
59	52, 58	syl6req 2515	. . . . . . . . . . . 12
60	47, 59	opeq12d 4225	. . . . . . . . . . 11
61	50	rneqd 5235	. . . . . . . . . . . . 13
62	61	unieqd 4259	. . . . . . . . . . . 12
63	54	rneqi 5234	. . . . . . . . . . . . . 14
64	63	unieqi 4258	. . . . . . . . . . . . 13
65	25, 19	op2nda 5498	. . . . . . . . . . . . 13
66	64, 65	eqtri 2486	. . . . . . . . . . . 12
67	62, 66	syl6req 2515	. . . . . . . . . . 11
68	60, 67	opeq12d 4225	. . . . . . . . . 10
69	41, 68	eq2tri 2525	. . . . . . . . 9
70		anass 649	. . . . . . . . 9
71	69, 70	anbi12i 697	. . . . . . . 8
72		an32 798	. . . . . . . 8
73		an32 798	. . . . . . . 8
74	71, 72, 73	3bitr4i 277	. . . . . . 7
75	74	exbii 1667	. . . . . 6
76		19.41v 1771	. . . . . 6
77		19.41v 1771	. . . . . 6
78	75, 76, 77	3bitr3i 275	. . . . 5
79	78	2exbii 1668	. . . 4
80		19.41vv 1772	. . . 4
81		19.41vv 1772	. . . 4
82	79, 80, 81	3bitr3i 275	. . 3
83		elxp 5021	. . . . 5
84		excom 1849	. . . . 5
85		elxp 5021	. . . . . . . . 9
86	85	anbi1i 695	. . . . . . . 8
87		an12 797	. . . . . . . 8
88		19.41vv 1772	. . . . . . . 8
89	86, 87, 88	3bitr4i 277	. . . . . . 7
90	89	2exbii 1668	. . . . . 6
91		exrot4 1853	. . . . . 6
92		anass 649	. . . . . . . . 9
93	92	exbii 1667	. . . . . . . 8
94		opeq1 4217	. . . . . . . . . . . 12
95	94	eqeq2d 2471	. . . . . . . . . . 11
96	95	anbi1d 704	. . . . . . . . . 10
97	96	anbi2d 703	. . . . . . . . 9
98	18, 97	ceqsexv 3146	. . . . . . . 8
99		an12 797	. . . . . . . 8
100	93, 98, 99	3bitri 271	. . . . . . 7
101	100	3exbii 1669	. . . . . 6
102	90, 91, 101	3bitri 271	. . . . 5
103	83, 84, 102	3bitri 271	. . . 4
104	103	anbi1i 695	. . 3
105		elxp 5021	. . . . 5
106		elxp 5021	. . . . . . . . . 10
107	106	anbi2i 694	. . . . . . . . 9
108		anass 649	. . . . . . . . 9
109		19.42vv 1777	. . . . . . . . . 10
110		an12 797	. . . . . . . . . . . 12
111		anass 649	. . . . . . . . . . . . 13
112	111	anbi2i 694	. . . . . . . . . . . 12
113	110, 112	bitri 249	. . . . . . . . . . 11
114	113	2exbii 1668	. . . . . . . . . 10
115	109, 114	bitr3i 251	. . . . . . . . 9
116	107, 108, 115	3bitr3i 275	. . . . . . . 8
117	116	exbii 1667	. . . . . . 7
118		exrot3 1852	. . . . . . 7
119		opeq2 4218	. . . . . . . . . . 11
120	119	eqeq2d 2471	. . . . . . . . . 10
121	120	anbi1d 704	. . . . . . . . 9
122	45, 121	ceqsexv 3146	. . . . . . . 8
123	122	2exbii 1668	. . . . . . 7
124	117, 118, 123	3bitri 271	. . . . . 6
125	124	exbii 1667	. . . . 5
126	105, 125	bitri 249	. . . 4
127	126	anbi1i 695	. . 3
128	82, 104, 127	3bitr4i 277	. 2
129	5, 7, 9, 11, 128	en2i 7573	1

Syntax hints:  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  cvv 3109  {csn 4029  <.cop 4035  U.cuni 4249   class class class wbr 4452  X.cxp 5002  domcdm 5004  rancrn 5005  cen 7533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-en 7537