Theorem xpeq2d 5023

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 5014	. 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 1379   X. cxp 4997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-opab 4506  df-xp 5005

This theorem is referenced by:  xpriindi  5139  csbres  5276  csbresgOLD  5277  fconstg  5772  curry2  6878  fparlem4  6886  fvdiagfn  7463  mapsncnv  7465  xpsneng  7602  xpcdaen  8563  axdc4lem  8835  fpwwe2lem13  9020  expval  12136  imasvscafn  14792  comfffval  14954  fuchom  15188  homafval  15214  setcmon  15272  xpccofval  15309  pwsco2mhm  15821  frmdplusg  15854  mulgfval  15953  mulgval  15954  symgplusg  16219  efgval  16541  psrplusg  17833  psrvscafval  17842  psrvsca  17843  opsrle  17939  evlssca  17990  mpfind  18004  coe1fv  18044  coe1tm  18113  pf1ind  18190  pjfval  18532  frlmval  18574  islindf5  18669  mdetunilem4  18912  mdetunilem9  18917  txindislem  19897  txcmplem2  19906  txhaus  19911  txkgen  19916  xkofvcn  19948  xkoinjcn  19951  cnextval  20324  cnextfval  20325  pcorev2  21291  pcophtb  21292  pi1grplem  21312  pi1inv  21315  dvfval  22064  dvnfval  22088  0dgrb  22406  dgreq0  22424  dgrmulc  22430  plyrem  22463  facth  22464  fta1  22466  aaliou2  22498  taylfval  22516  taylpfval  22522  gxval  24964  0ofval  25406  indval2  27696  sxbrsigalem3  27911  sxbrsigalem2  27925  eulerpartlemgu  27984  sseqval  27995  sconpht  28342  sconpht2  28351  sconpi1  28352  cvmlift2lem11  28426  cvmlift2lem12  28427  cvmlift2lem13  28428  cvmlift3lem9  28440  elima4  28814  ismrer1  29965  mzpclval  30289  mzpcl1  30293  dgrnznn  30717  mendvsca  30773  dvconstbi  30867  expgrowth  30868  bj-xtageq  33645  lflsc0N  33898  lkrscss  33913  lfl1dim  33936  lfl1dim2N  33937  ldualvs  33952