Theorem xpeq2d 5139

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 5129	. 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 1483   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-opab 4713  df-xp 5120

This theorem is referenced by:  xpriindi  5258  csbres  5399  fconstg  6092  curry2  7272  fparlem4  7280  fvdiagfn  7902  mapsncnv  7904  xpsneng  8045  xpcdaen  9005  axdc4lem  9277  fpwwe2lem13  9464  expval  12862  imasvscafn  16197  comfffval  16358  fuchom  16621  homafval  16679  setcmon  16737  xpccofval  16822  pwsco2mhm  17371  frmdplusg  17391  mulgfval  17542  mulgval  17543  symgplusg  17809  efgval  18130  psrplusg  19381  psrvscafval  19390  psrvsca  19391  opsrle  19475  evlssca  19522  mpfind  19536  coe1fv  19576  coe1tm  19643  pf1ind  19719  pjfval  20050  frlmval  20092  islindf5  20178  mdetunilem4  20421  mdetunilem9  20426  txindislem  21436  txcmplem2  21445  txhaus  21450  txkgen  21455  xkofvcn  21487  xkoinjcn  21490  cnextval  21865  cnextfval  21866  pcorev2  22828  pcophtb  22829  pi1grplem  22849  pi1inv  22852  dvfval  23661  dvnfval  23685  0dgrb  24002  dgrnznn  24003  dgreq0  24021  dgrmulc  24027  plyrem  24060  facth  24061  fta1  24063  aaliou2  24095  taylfval  24113  taylpfval  24119  0ofval  27642  aciunf1  29463  indval2  30076  sxbrsigalem3  30334  sxbrsigalem2  30348  eulerpartlemgu  30439  sseqval  30450  sconnpht  31211  sconnpht2  31220  sconnpi1  31221  cvmlift2lem11  31295  cvmlift2lem12  31296  cvmlift2lem13  31297  cvmlift3lem9  31309  mexval  31399  mexval2  31400  mdvval  31401  mpstval  31432  elima4  31679  bj-xtageq  32976  matunitlindflem1  33405  poimirlem32  33441  ismrer1  33637  lflsc0N  34370  lkrscss  34385  lfl1dim  34408  lfl1dim2N  34409  ldualvs  34424  mzpclval  37288  mzpcl1  37292  mendvsca  37761  dvconstbi  38533  expgrowth  38534  csbresgOLD  39055