MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpeq2d Structured version   Visualization version   GIF version

Theorem xpeq2d 5584
Description: Equality deduction for Cartesian product. (Contributed by Jeff Madsen, 17-Jun-2010.)
Hypothesis
Ref Expression
xpeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
xpeq2d (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Proof of Theorem xpeq2d
StepHypRef Expression
1 xpeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 xpeq2 5575 . 2 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
31, 2syl 17 1 (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530   × cxp 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-opab 5126  df-xp 5560
This theorem is referenced by:  xpriindi  5706  csbres  5855  fconstg  6563  curry2  7793  fparlem4  7801  fvdiagfn  8444  mapsncnv  8446  xpsneng  8591  axdc4lem  9866  fpwwe2lem13  10053  expval  13421  imasvscafn  16800  comfffval  16958  fuchom  17221  homafval  17279  setcmon  17337  xpccofval  17422  pwsco2mhm  17980  frmdplusg  18002  mulgfval  18156  mulgfvalALT  18157  mulgval  18158  symgplusg  18437  efgval  18763  psrplusg  20080  psrvscafval  20089  psrvsca  20090  opsrle  20174  evlssca  20220  mpfind  20237  coe1fv  20291  coe1tm  20358  pf1ind  20434  pjfval  20766  frlmval  20808  islindf5  20899  mdetunilem4  21140  mdetunilem9  21145  txindislem  22157  txcmplem2  22166  txhaus  22171  txkgen  22176  xkofvcn  22208  xkoinjcn  22211  cnextval  22585  cnextfval  22586  pcorev2  23547  pcophtb  23548  pi1grplem  23568  pi1inv  23571  dvfval  24410  dvnfval  24434  0dgrb  24751  dgrnznn  24752  dgreq0  24770  dgrmulc  24776  plyrem  24809  facth  24810  fta1  24812  aaliou2  24844  taylfval  24862  taylpfval  24868  0ofval  28478  aciunf1  30323  hashxpe  30442  indval2  31159  sxbrsigalem3  31416  sxbrsigalem2  31430  eulerpartlemgu  31521  sseqval  31532  sconnpht  32360  sconnpht2  32369  sconnpi1  32370  cvmlift2lem11  32444  cvmlift2lem12  32445  cvmlift2lem13  32446  cvmlift3lem9  32458  sat1el2xp  32510  mexval  32633  mexval2  32634  mdvval  32635  mpstval  32666  elima4  32903  bj-xtageq  34184  matunitlindflem1  34755  poimirlem32  34791  ismrer1  34984  lflsc0N  36086  lkrscss  36101  lfl1dim  36124  lfl1dim2N  36125  ldualvs  36140  0prjspnrel  39134  mzpclval  39187  mzpcl1  39191  mendvsca  39656  dvconstbi  40531  expgrowth  40532
  Copyright terms: Public domain W3C validator