Theorem xpeq2d 5012

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 5003	. 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 1398   X. cxp 4986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-opab 4498  df-xp 4994

This theorem is referenced by:  xpriindi  5128  csbres  5265  fconstg  5754  curry2  6868  fparlem4  6876  fvdiagfn  7456  mapsncnv  7458  xpsneng  7595  xpcdaen  8554  axdc4lem  8826  fpwwe2lem13  9009  expval  12150  imasvscafn  15026  comfffval  15186  fuchom  15449  homafval  15507  setcmon  15565  xpccofval  15650  pwsco2mhm  16201  frmdplusg  16221  mulgfval  16342  mulgval  16343  symgplusg  16613  efgval  16934  psrplusg  18229  psrvscafval  18238  psrvsca  18239  opsrle  18335  evlssca  18386  mpfind  18400  coe1fv  18440  coe1tm  18509  pf1ind  18586  pjfval  18910  frlmval  18952  islindf5  19041  mdetunilem4  19284  mdetunilem9  19289  txindislem  20300  txcmplem2  20309  txhaus  20314  txkgen  20319  xkofvcn  20351  xkoinjcn  20354  cnextval  20727  cnextfval  20728  pcorev2  21694  pcophtb  21695  pi1grplem  21715  pi1inv  21718  dvfval  22467  dvnfval  22491  0dgrb  22809  dgrnznn  22810  dgreq0  22828  dgrmulc  22834  plyrem  22867  facth  22868  fta1  22870  aaliou2  22902  taylfval  22920  taylpfval  22926  gxval  25458  0ofval  25900  aciunf1  27730  indval2  28244  sxbrsigalem3  28480  sxbrsigalem2  28494  eulerpartlemgu  28580  sseqval  28591  sconpht  28938  sconpht2  28947  sconpi1  28948  cvmlift2lem11  29022  cvmlift2lem12  29023  cvmlift2lem13  29024  cvmlift3lem9  29036  mexval  29126  mexval2  29127  mdvval  29128  mpstval  29159  elima4  29449  ismrer1  30574  mzpclval  30897  mzpcl1  30901  mendvsca  31381  dvconstbi  31480  expgrowth  31481  csbresgOLD  34020  bj-xtageq  34947  lflsc0N  35205  lkrscss  35220  lfl1dim  35243  lfl1dim2N  35244  ldualvs  35259