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

Theorem xpeq2d 5578
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 5569 . 2 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
31, 2syl 17 1 (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528   × cxp 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-opab 5120  df-xp 5554
This theorem is referenced by:  xpriindi  5700  csbres  5849  fconstg  6559  curry2  7791  fparlem4  7799  fvdiagfn  8443  mapsncnv  8445  xpsneng  8590  axdc4lem  9865  fpwwe2lem13  10052  expval  13419  imasvscafn  16798  fuchom  17219  homafval  17277  setcmon  17335  pwsco2mhm  17985  frmdplusg  18007  mulgfval  18164  mulgfvalALT  18165  mulgval  18166  efgval  18772  psrplusg  20089  psrvscafval  20098  psrvsca  20099  opsrle  20184  evlssca  20230  mpfind  20248  coe1fv  20302  coe1tm  20369  pf1ind  20446  pjfval  20778  frlmval  20820  islindf5  20911  mdetunilem4  21152  mdetunilem9  21157  txindislem  22169  txcmplem2  22178  txhaus  22183  txkgen  22188  xkofvcn  22220  xkoinjcn  22223  cnextval  22597  cnextfval  22598  pcorev2  23559  pcophtb  23560  pi1grplem  23580  pi1inv  23583  dvfval  24422  dvnfval  24446  0dgrb  24763  dgrnznn  24764  dgreq0  24782  dgrmulc  24788  plyrem  24821  facth  24822  fta1  24824  aaliou2  24856  taylfval  24874  taylpfval  24880  0ofval  28491  aciunf1  30336  hashxpe  30455  indval2  31172  sxbrsigalem3  31429  sxbrsigalem2  31443  eulerpartlemgu  31534  sseqval  31545  sconnpht  32373  sconnpht2  32382  sconnpi1  32383  cvmlift2lem11  32457  cvmlift2lem12  32458  cvmlift2lem13  32459  cvmlift3lem9  32471  sat1el2xp  32523  mexval  32646  mexval2  32647  mdvval  32648  mpstval  32679  elima4  32916  bj-xtageq  34197  matunitlindflem1  34769  poimirlem32  34805  ismrer1  34997  lflsc0N  36099  lkrscss  36114  lfl1dim  36137  lfl1dim2N  36138  ldualvs  36153  0prjspnrel  39147  mzpclval  39200  mzpcl1  39204  mendvsca  39669  dvconstbi  40543  expgrowth  40544  smndex1igid  44004
  Copyright terms: Public domain W3C validator