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

Theorem xpeq2d 5052
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 5042 . 2 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
31, 2syl 17 1 (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474   × cxp 5025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-opab 4638  df-xp 5033
This theorem is referenced by:  xpriindi  5167  csbres  5306  fconstg  5989  curry2  7136  fparlem4  7144  fvdiagfn  7765  mapsncnv  7767  xpsneng  7907  xpcdaen  8865  axdc4lem  9137  fpwwe2lem13  9320  expval  12681  imasvscafn  15968  comfffval  16129  fuchom  16392  homafval  16450  setcmon  16508  xpccofval  16593  pwsco2mhm  17142  frmdplusg  17162  mulgfval  17313  mulgval  17314  symgplusg  17580  efgval  17901  psrplusg  19150  psrvscafval  19159  psrvsca  19160  opsrle  19244  evlssca  19291  mpfind  19305  coe1fv  19345  coe1tm  19412  pf1ind  19488  pjfval  19816  frlmval  19858  islindf5  19944  mdetunilem4  20187  mdetunilem9  20192  txindislem  21193  txcmplem2  21202  txhaus  21207  txkgen  21212  xkofvcn  21244  xkoinjcn  21247  cnextval  21622  cnextfval  21623  pcorev2  22583  pcophtb  22584  pi1grplem  22604  pi1inv  22607  dvfval  23411  dvnfval  23435  0dgrb  23750  dgrnznn  23751  dgreq0  23769  dgrmulc  23775  plyrem  23808  facth  23809  fta1  23811  aaliou2  23843  taylfval  23861  taylpfval  23867  0ofval  26819  aciunf1  28638  indval2  29197  sxbrsigalem3  29454  sxbrsigalem2  29468  eulerpartlemgu  29559  sseqval  29570  sconpht  30258  sconpht2  30267  sconpi1  30268  cvmlift2lem11  30342  cvmlift2lem12  30343  cvmlift2lem13  30344  cvmlift3lem9  30356  mexval  30446  mexval2  30447  mdvval  30448  mpstval  30479  elima4  30717  bj-xtageq  31952  matunitlindflem1  32358  poimirlem32  32394  ismrer1  32590  lflsc0N  33171  lkrscss  33186  lfl1dim  33209  lfl1dim2N  33210  ldualvs  33225  mzpclval  36089  mzpcl1  36093  mendvsca  36563  dvconstbi  37338  expgrowth  37339  csbresgOLD  37860
  Copyright terms: Public domain W3C validator