Theorem xpeq2d 5549

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

Step	Hyp	Ref	Expression
1		xpeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		xpeq2 5540	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Syntax hints:   → wi 4   = wceq 1538   × cxp 5517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-opab 5093  df-xp 5525

This theorem is referenced by:  xpriindi  5671  csbres  5821  fconstg  6540  curry2  7785  fparlem4  7793  fvdiagfn  8438  mapsncnv  8440  xpsneng  8585  axdc4lem  9866  fpwwe2lem13  10053  expval  13427  imasvscafn  16802  fuchom  17223  homafval  17281  setcmon  17339  pwsco2mhm  17989  frmdplusg  18011  smndex1igid  18061  mulgfval  18218  mulgfvalALT  18219  mulgval  18220  efgval  18835  pjfval  20395  frlmval  20437  islindf5  20528  psrplusg  20619  psrvscafval  20628  psrvsca  20629  opsrle  20715  evlssca  20761  mpfind  20779  coe1fv  20835  coe1tm  20902  pf1ind  20979  mdetunilem4  21220  mdetunilem9  21225  txindislem  22238  txcmplem2  22247  txhaus  22252  txkgen  22257  xkofvcn  22289  xkoinjcn  22292  cnextval  22666  cnextfval  22667  pcorev2  23633  pcophtb  23634  pi1grplem  23654  pi1inv  23657  dvfval  24500  dvnfval  24525  0dgrb  24843  dgrnznn  24844  dgreq0  24862  dgrmulc  24868  plyrem  24901  facth  24902  fta1  24904  aaliou2  24936  taylfval  24954  taylpfval  24960  0ofval  28570  2ndresdju  30411  aciunf1  30426  hashxpe  30555  gsumpart  30740  indval2  31383  sxbrsigalem3  31640  sxbrsigalem2  31654  eulerpartlemgu  31745  sseqval  31756  sconnpht  32589  sconnpht2  32598  sconnpi1  32599  cvmlift2lem11  32673  cvmlift2lem12  32674  cvmlift2lem13  32675  cvmlift3lem9  32687  sat1el2xp  32739  mexval  32862  mexval2  32863  mdvval  32864  mpstval  32895  elima4  33132  bj-xtageq  34424  matunitlindflem1  35053  poimirlem32  35089  ismrer1  35276  lflsc0N  36379  lkrscss  36394  lfl1dim  36417  lfl1dim2N  36418  ldualvs  36433  0prjspnrel  39613  mzpclval  39666  mzpcl1  39670  mendvsca  40135  dvconstbi  41038  expgrowth  41039