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

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

Syntax hints:   → wi 4   = wceq 1531   × cxp 5546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-opab 5120  df-xp 5554

This theorem is referenced by:  xpriindi  5700  csbres  5849  fconstg  6559  curry2  7794  fparlem4  7802  fvdiagfn  8447  mapsncnv  8449  xpsneng  8594  axdc4lem  9869  fpwwe2lem13  10056  expval  13423  imasvscafn  16802  fuchom  17223  homafval  17281  setcmon  17339  pwsco2mhm  17989  frmdplusg  18011  smndex1igid  18061  mulgfval  18218  mulgfvalALT  18219  mulgval  18220  efgval  18835  psrplusg  20153  psrvscafval  20162  psrvsca  20163  opsrle  20248  evlssca  20294  mpfind  20312  coe1fv  20366  coe1tm  20433  pf1ind  20510  pjfval  20842  frlmval  20884  islindf5  20975  mdetunilem4  21216  mdetunilem9  21221  txindislem  22233  txcmplem2  22242  txhaus  22247  txkgen  22252  xkofvcn  22284  xkoinjcn  22287  cnextval  22661  cnextfval  22662  pcorev2  23624  pcophtb  23625  pi1grplem  23645  pi1inv  23648  dvfval  24487  dvnfval  24511  0dgrb  24828  dgrnznn  24829  dgreq0  24847  dgrmulc  24853  plyrem  24886  facth  24887  fta1  24889  aaliou2  24921  taylfval  24939  taylpfval  24945  0ofval  28556  aciunf1  30400  hashxpe  30521  indval2  31266  sxbrsigalem3  31523  sxbrsigalem2  31537  eulerpartlemgu  31628  sseqval  31639  sconnpht  32469  sconnpht2  32478  sconnpi1  32479  cvmlift2lem11  32553  cvmlift2lem12  32554  cvmlift2lem13  32555  cvmlift3lem9  32567  sat1el2xp  32619  mexval  32742  mexval2  32743  mdvval  32744  mpstval  32775  elima4  33012  bj-xtageq  34293  matunitlindflem1  34880  poimirlem32  34916  ismrer1  35108  lflsc0N  36211  lkrscss  36226  lfl1dim  36249  lfl1dim2N  36250  ldualvs  36265  0prjspnrel  39259  mzpclval  39312  mzpcl1  39316  mendvsca  39781  dvconstbi  40656  expgrowth  40657