Theorem xpeq2d 4880

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 4871	. 2 |- ( A = B -> ( C X. A ) = ( C X. B ) )
3	1, 2	syl 17	1 |- ( ph -> ( C X. A ) = ( C X. B ) )

Syntax hints:   -> wi 4   = wceq 1455   X. cxp 4854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-opab 4478  df-xp 4862

This theorem is referenced by:  xpriindi  4993  csbres  5130  fconstg  5797  curry2  6923  fparlem4  6931  fvdiagfn  7547  mapsncnv  7549  xpsneng  7688  xpcdaen  8644  axdc4lem  8916  fpwwe2lem13  9098  expval  12312  imasvscafn  15498  comfffval  15658  fuchom  15921  homafval  15979  setcmon  16037  xpccofval  16122  pwsco2mhm  16673  frmdplusg  16693  mulgfval  16814  mulgval  16815  symgplusg  17085  efgval  17422  psrplusg  18660  psrvscafval  18669  psrvsca  18670  opsrle  18754  evlssca  18800  mpfind  18814  coe1fv  18854  coe1tm  18921  pf1ind  18998  pjfval  19324  frlmval  19366  islindf5  19452  mdetunilem4  19695  mdetunilem9  19700  txindislem  20703  txcmplem2  20712  txhaus  20717  txkgen  20722  xkofvcn  20754  xkoinjcn  20757  cnextval  21131  cnextfval  21132  pcorev2  22114  pcophtb  22115  pi1grplem  22135  pi1inv  22138  dvfval  22908  dvnfval  22932  0dgrb  23256  dgrnznn  23257  dgreq0  23275  dgrmulc  23281  plyrem  23314  facth  23315  fta1  23317  aaliou2  23352  taylfval  23370  taylpfval  23376  gxval  26042  0ofval  26484  aciunf1  28317  indval2  28887  sxbrsigalem3  29144  sxbrsigalem2  29158  eulerpartlemgu  29260  sseqval  29271  sconpht  30002  sconpht2  30011  sconpi1  30012  cvmlift2lem11  30086  cvmlift2lem12  30087  cvmlift2lem13  30088  cvmlift3lem9  30100  mexval  30190  mexval2  30191  mdvval  30192  mpstval  30223  elima4  30471  bj-xtageq  31628  poimirlem32  32018  ismrer1  32216  lflsc0N  32695  lkrscss  32710  lfl1dim  32733  lfl1dim2N  32734  ldualvs  32749  mzpclval  35613  mzpcl1  35617  mendvsca  36103  dvconstbi  36728  expgrowth  36729  csbresgOLD  37257