Theorem xpeq2d 4885

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 4876	. 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 1369   X. cxp 4859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-opab 4372  df-xp 4867

This theorem is referenced by:  xpriindi  4997  csbres  5134  csbresgOLD  5135  fconstg  5618  curry2  6688  fparlem4  6696  fvdiagfn  7278  mapsncnv  7280  xpsneng  7417  xpcdaen  8373  axdc4lem  8645  fpwwe2lem13  8830  expval  11888  imasvscafn  14496  comfffval  14658  fuchom  14892  homafval  14918  setcmon  14976  xpccofval  15013  pwsco2mhm  15520  frmdplusg  15553  mulgfval  15649  mulgval  15650  symgplusg  15915  efgval  16235  psrplusg  17474  psrvscafval  17483  psrvsca  17484  opsrle  17579  evlssca  17630  mpfind  17644  coe1fv  17684  coe1tm  17748  pf1ind  17811  pjfval  18153  frlmval  18195  islindf5  18290  mdetunilem4  18443  mdetunilem9  18448  txindislem  19228  txcmplem2  19237  txhaus  19242  txkgen  19247  xkofvcn  19279  xkoinjcn  19282  cnextval  19655  cnextfval  19656  pcorev2  20622  pcophtb  20623  pi1grplem  20643  pi1inv  20646  dvfval  21394  dvnfval  21418  0dgrb  21736  dgreq0  21754  dgrmulc  21760  plyrem  21793  facth  21794  fta1  21796  aaliou2  21828  taylfval  21846  taylpfval  21852  gxval  23767  0ofval  24209  indval2  26493  sxbrsigalem3  26709  sxbrsigalem2  26723  eulerpartlemgu  26782  sseqval  26793  sconpht  27140  sconpht2  27149  sconpi1  27150  cvmlift2lem11  27224  cvmlift2lem12  27225  cvmlift2lem13  27226  cvmlift3lem9  27238  elima4  27612  ismrer1  28763  mzpclval  29087  mzpcl1  29091  dgrnznn  29518  mendvsca  29574  dvconstbi  29634  expgrowth  29635  bj-xtageq  32577  lflsc0N  32824  lkrscss  32839  lfl1dim  32862  lfl1dim2N  32863  ldualvs  32878