Theorem xpeq2d 4873

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 4864	. 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 1437   X. cxp 4847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-opab 4480  df-xp 4855

This theorem is referenced by:  xpriindi  4986  csbres  5123  fconstg  5783  curry2  6898  fparlem4  6906  fvdiagfn  7520  mapsncnv  7522  xpsneng  7659  xpcdaen  8613  axdc4lem  8885  fpwwe2lem13  9067  expval  12273  imasvscafn  15428  comfffval  15588  fuchom  15851  homafval  15909  setcmon  15967  xpccofval  16052  pwsco2mhm  16603  frmdplusg  16623  mulgfval  16744  mulgval  16745  symgplusg  17015  efgval  17352  psrplusg  18590  psrvscafval  18599  psrvsca  18600  opsrle  18684  evlssca  18730  mpfind  18744  coe1fv  18784  coe1tm  18851  pf1ind  18928  pjfval  19253  frlmval  19295  islindf5  19381  mdetunilem4  19624  mdetunilem9  19629  txindislem  20632  txcmplem2  20641  txhaus  20646  txkgen  20651  xkofvcn  20683  xkoinjcn  20686  cnextval  21060  cnextfval  21061  pcorev2  22043  pcophtb  22044  pi1grplem  22064  pi1inv  22067  dvfval  22836  dvnfval  22860  0dgrb  23184  dgrnznn  23185  dgreq0  23203  dgrmulc  23209  plyrem  23242  facth  23243  fta1  23245  aaliou2  23280  taylfval  23298  taylpfval  23304  gxval  25969  0ofval  26411  aciunf1  28252  indval2  28829  sxbrsigalem3  29087  sxbrsigalem2  29101  eulerpartlemgu  29203  sseqval  29214  sconpht  29945  sconpht2  29954  sconpi1  29955  cvmlift2lem11  30029  cvmlift2lem12  30030  cvmlift2lem13  30031  cvmlift3lem9  30043  mexval  30133  mexval2  30134  mdvval  30135  mpstval  30166  elima4  30413  bj-xtageq  31535  poimirlem32  31883  ismrer1  32081  lflsc0N  32565  lkrscss  32580  lfl1dim  32603  lfl1dim2N  32604  ldualvs  32619  mzpclval  35483  mzpcl1  35487  mendvsca  35974  dvconstbi  36538  expgrowth  36539  csbresgOLD  37074