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

Theorem xpiindi 4989
 Description: Distributive law for Cartesian product over indexed intersection. (Contributed by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
xpiindi
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem xpiindi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relxp 4961 . . . . . 6
21rgenw 2783 . . . . 5
3 r19.2z 3888 . . . . 5
42, 3mpan2 675 . . . 4
5 reliin 4974 . . . 4
64, 5syl 17 . . 3
7 relxp 4961 . . 3
86, 7jctil 539 . 2
9 r19.28zv 3894 . . . . . 6
109bicomd 204 . . . . 5
11 vex 3083 . . . . . . 7
12 eliin 4305 . . . . . . 7
1311, 12ax-mp 5 . . . . . 6
1413anbi2i 698 . . . . 5
15 opelxp 4883 . . . . . 6
1615ralbii 2853 . . . . 5
1710, 14, 163bitr4g 291 . . . 4
18 opelxp 4883 . . . 4
19 opex 4685 . . . . 5
20 eliin 4305 . . . . 5
2119, 20ax-mp 5 . . . 4
2217, 18, 213bitr4g 291 . . 3
2322eqrelrdv2 4953 . 2
248, 23mpancom 673 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   wceq 1437   wcel 1872   wne 2614  wral 2771  wrex 2772  cvv 3080  c0 3761  cop 4004  ciin 4300   cxp 4851   wrel 4858 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-iin 4302  df-opab 4483  df-xp 4859  df-rel 4860 This theorem is referenced by:  xpriindi  4990
 Copyright terms: Public domain W3C validator