MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpassen Unicode version

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.
StepHypRef Expression
1 xpassen.1 . . . 4
2 xpassen.2 . . . 4
31, 2xpex 6604 . . 3
4 xpassen.3 . . 3
53, 4xpex 6604 . 2
62, 4xpex 6604 . . 3
71, 6xpex 6604 . 2
8 opex 4716 . . 3
98a1i 11 . 2
10 opex 4716 . . 3
1110a1i 11 . 2
12 sneq 4039 . . . . . . . . . . . . . . . . 17
1312dmeqd 5210 . . . . . . . . . . . . . . . 16
1413unieqd 4259 . . . . . . . . . . . . . . 15
1514sneqd 4041 . . . . . . . . . . . . . 14
1615dmeqd 5210 . . . . . . . . . . . . 13
1716unieqd 4259 . . . . . . . . . . . 12
18 opex 4716 . . . . . . . . . . . . . . . . 17
19 vex 3112 . . . . . . . . . . . . . . . . 17
2018, 19op1sta 5495 . . . . . . . . . . . . . . . 16
2120sneqi 4040 . . . . . . . . . . . . . . 15
2221dmeqi 5209 . . . . . . . . . . . . . 14
2322unieqi 4258 . . . . . . . . . . . . 13
24 vex 3112 . . . . . . . . . . . . . 14
25 vex 3112 . . . . . . . . . . . . . 14
2624, 25op1sta 5495 . . . . . . . . . . . . 13
2723, 26eqtri 2486 . . . . . . . . . . . 12
2817, 27syl6req 2515 . . . . . . . . . . 11
2915rneqd 5235 . . . . . . . . . . . . . 14
3029unieqd 4259 . . . . . . . . . . . . 13
3121rneqi 5234 . . . . . . . . . . . . . . 15
3231unieqi 4258 . . . . . . . . . . . . . 14
3324, 25op2nda 5498 . . . . . . . . . . . . . 14
3432, 33eqtri 2486 . . . . . . . . . . . . 13
3530, 34syl6req 2515 . . . . . . . . . . . 12
3612rneqd 5235 . . . . . . . . . . . . . 14
3736unieqd 4259 . . . . . . . . . . . . 13
3818, 19op2nda 5498 . . . . . . . . . . . . 13
3937, 38syl6req 2515 . . . . . . . . . . . 12
4035, 39opeq12d 4225 . . . . . . . . . . 11
4128, 40opeq12d 4225 . . . . . . . . . 10
42 sneq 4039 . . . . . . . . . . . . . . 15
4342dmeqd 5210 . . . . . . . . . . . . . 14
4443unieqd 4259 . . . . . . . . . . . . 13
45 opex 4716 . . . . . . . . . . . . . 14
4624, 45op1sta 5495 . . . . . . . . . . . . 13
4744, 46syl6req 2515 . . . . . . . . . . . 12
4842rneqd 5235 . . . . . . . . . . . . . . . . 17
4948unieqd 4259 . . . . . . . . . . . . . . . 16
5049sneqd 4041 . . . . . . . . . . . . . . 15
5150dmeqd 5210 . . . . . . . . . . . . . 14
5251unieqd 4259 . . . . . . . . . . . . 13
5324, 45op2nda 5498 . . . . . . . . . . . . . . . . 17
5453sneqi 4040 . . . . . . . . . . . . . . . 16
5554dmeqi 5209 . . . . . . . . . . . . . . 15
5655unieqi 4258 . . . . . . . . . . . . . 14
5725, 19op1sta 5495 . . . . . . . . . . . . . 14
5856, 57eqtri 2486 . . . . . . . . . . . . 13
5952, 58syl6req 2515 . . . . . . . . . . . 12
6047, 59opeq12d 4225 . . . . . . . . . . 11
6150rneqd 5235 . . . . . . . . . . . . 13
6261unieqd 4259 . . . . . . . . . . . 12
6354rneqi 5234 . . . . . . . . . . . . . 14
6463unieqi 4258 . . . . . . . . . . . . 13
6525, 19op2nda 5498 . . . . . . . . . . . . 13
6664, 65eqtri 2486 . . . . . . . . . . . 12
6762, 66syl6req 2515 . . . . . . . . . . 11
6860, 67opeq12d 4225 . . . . . . . . . 10
6941, 68eq2tri 2525 . . . . . . . . 9
70 anass 649 . . . . . . . . 9
7169, 70anbi12i 697 . . . . . . . 8
72 an32 798 . . . . . . . 8
73 an32 798 . . . . . . . 8
7471, 72, 733bitr4i 277 . . . . . . 7
7574exbii 1667 . . . . . 6
76 19.41v 1771 . . . . . 6
77 19.41v 1771 . . . . . 6
7875, 76, 773bitr3i 275 . . . . 5
79782exbii 1668 . . . 4
80 19.41vv 1772 . . . 4
81 19.41vv 1772 . . . 4
8279, 80, 813bitr3i 275 . . 3
83 elxp 5021 . . . . 5
84 excom 1849 . . . . 5
85 elxp 5021 . . . . . . . . 9
8685anbi1i 695 . . . . . . . 8
87 an12 797 . . . . . . . 8
88 19.41vv 1772 . . . . . . . 8
8986, 87, 883bitr4i 277 . . . . . . 7
90892exbii 1668 . . . . . 6
91 exrot4 1853 . . . . . 6
92 anass 649 . . . . . . . . 9
9392exbii 1667 . . . . . . . 8
94 opeq1 4217 . . . . . . . . . . . 12
9594eqeq2d 2471 . . . . . . . . . . 11
9695anbi1d 704 . . . . . . . . . 10
9796anbi2d 703 . . . . . . . . 9
9818, 97ceqsexv 3146 . . . . . . . 8
99 an12 797 . . . . . . . 8
10093, 98, 993bitri 271 . . . . . . 7
1011003exbii 1669 . . . . . 6
10290, 91, 1013bitri 271 . . . . 5
10383, 84, 1023bitri 271 . . . 4
104103anbi1i 695 . . 3
105 elxp 5021 . . . . 5
106 elxp 5021 . . . . . . . . . 10
107106anbi2i 694 . . . . . . . . 9
108 anass 649 . . . . . . . . 9
109 19.42vv 1777 . . . . . . . . . 10
110 an12 797 . . . . . . . . . . . 12
111 anass 649 . . . . . . . . . . . . 13
112111anbi2i 694 . . . . . . . . . . . 12
113110, 112bitri 249 . . . . . . . . . . 11
1141132exbii 1668 . . . . . . . . . 10
115109, 114bitr3i 251 . . . . . . . . 9
116107, 108, 1153bitr3i 275 . . . . . . . 8
117116exbii 1667 . . . . . . 7
118 exrot3 1852 . . . . . . 7
119 opeq2 4218 . . . . . . . . . . 11
120119eqeq2d 2471 . . . . . . . . . 10
121120anbi1d 704 . . . . . . . . 9
12245, 121ceqsexv 3146 . . . . . . . 8
1231222exbii 1668 . . . . . . 7
124117, 118, 1233bitri 271 . . . . . 6
125124exbii 1667 . . . . 5
126105, 125bitri 249 . . . 4
127126anbi1i 695 . . 3
12882, 104, 1273bitr4i 277 . 2
1295, 7, 9, 11, 128en2i 7573 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator