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

Theorem xpeq2d 5173
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 5163 . 2 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
31, 2syl 17 1 (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523   × cxp 5141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-opab 4746  df-xp 5149
This theorem is referenced by:  xpriindi  5291  csbres  5431  fconstg  6130  curry2  7317  fparlem4  7325  fvdiagfn  7944  mapsncnv  7946  xpsneng  8086  xpcdaen  9043  axdc4lem  9315  fpwwe2lem13  9502  expval  12902  imasvscafn  16244  comfffval  16405  fuchom  16668  homafval  16726  setcmon  16784  xpccofval  16869  pwsco2mhm  17418  frmdplusg  17438  mulgfval  17589  mulgval  17590  symgplusg  17855  efgval  18176  psrplusg  19429  psrvscafval  19438  psrvsca  19439  opsrle  19523  evlssca  19570  mpfind  19584  coe1fv  19624  coe1tm  19691  pf1ind  19767  pjfval  20098  frlmval  20140  islindf5  20226  mdetunilem4  20469  mdetunilem9  20474  txindislem  21484  txcmplem2  21493  txhaus  21498  txkgen  21503  xkofvcn  21535  xkoinjcn  21538  cnextval  21912  cnextfval  21913  pcorev2  22874  pcophtb  22875  pi1grplem  22895  pi1inv  22898  dvfval  23706  dvnfval  23730  0dgrb  24047  dgrnznn  24048  dgreq0  24066  dgrmulc  24072  plyrem  24105  facth  24106  fta1  24108  aaliou2  24140  taylfval  24158  taylpfval  24164  0ofval  27770  aciunf1  29591  indval2  30204  sxbrsigalem3  30462  sxbrsigalem2  30476  eulerpartlemgu  30567  sseqval  30578  sconnpht  31337  sconnpht2  31346  sconnpi1  31347  cvmlift2lem11  31421  cvmlift2lem12  31422  cvmlift2lem13  31423  cvmlift3lem9  31435  mexval  31525  mexval2  31526  mdvval  31527  mpstval  31558  elima4  31803  bj-xtageq  33101  matunitlindflem1  33535  poimirlem32  33571  ismrer1  33767  lflsc0N  34688  lkrscss  34703  lfl1dim  34726  lfl1dim2N  34727  ldualvs  34742  mzpclval  37605  mzpcl1  37609  mendvsca  38078  dvconstbi  38850  expgrowth  38851  csbresgOLD  39370
  Copyright terms: Public domain W3C validator