Theorem xpeq2d 4851

Description: Equality deduction for Cartesian product. (Contributed by Jeff Madsen, 17-Jun-2010.)

Hypothesis

Ref	Expression
xpeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
xpeq2d	|- ( ph -> ( C X. A ) = ( C X. B ) )

Proof of Theorem xpeq2d

Step	Hyp	Ref	Expression
1		xpeq1d.1	. 2 |- ( ph -> A = B )
2		xpeq2 4842	. 2 |- ( A = B -> ( C X. A ) = ( C X. B ) )
3	1, 2	syl 16	1 |- ( ph -> ( C X. A ) = ( C X. B ) )

Syntax hints:   -> wi 4   = wceq 1362   X. cxp 4825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-opab 4339  df-xp 4833

This theorem is referenced by:  xpriindi  4963  csbres  5100  csbresgOLD  5101  fconstg  5585  curry2  6656  fparlem4  6664  fvdiagfn  7245  mapsncnv  7247  xpsneng  7384  xpcdaen  8340  axdc4lem  8612  fpwwe2lem13  8796  expval  11850  imasvscafn  14457  comfffval  14619  fuchom  14853  homafval  14879  setcmon  14937  xpccofval  14974  pwsco2mhm  15480  frmdplusg  15511  mulgfval  15607  mulgval  15608  symgplusg  15873  efgval  16193  psrplusg  17385  psrvscafval  17394  psrvsca  17395  opsrle  17488  coe1fv  17560  coe1tm  17623  pjfval  17972  frlmval  18014  islindf5  18109  mdetunilem4  18262  mdetunilem9  18267  txindislem  19047  txcmplem2  19056  txhaus  19061  txkgen  19066  xkofvcn  19098  xkoinjcn  19101  cnextval  19474  cnextfval  19475  pcorev2  20441  pcophtb  20442  pi1grplem  20462  pi1inv  20465  dvfval  21213  dvnfval  21237  evlssca  21373  mpfind  21395  pf1ind  21405  0dgrb  21598  dgreq0  21616  dgrmulc  21622  plyrem  21655  facth  21656  fta1  21658  aaliou2  21690  taylfval  21708  taylpfval  21714  gxval  23567  0ofval  24009  indval2  26324  sxbrsigalem3  26540  sxbrsigalem2  26554  eulerpartlemgu  26607  sseqval  26618  sconpht  26965  sconpht2  26974  sconpi1  26975  cvmlift2lem11  27049  cvmlift2lem12  27050  cvmlift2lem13  27051  cvmlift3lem9  27063  elima4  27436  ismrer1  28578  mzpclval  28903  mzpcl1  28907  dgrnznn  29334  mendvsca  29390  dvconstbi  29450  expgrowth  29451  bj-xtageq  32061  lflsc0N  32298  lkrscss  32313  lfl1dim  32336  lfl1dim2N  32337  ldualvs  32352