MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpeq1d Structured version   Unicode version

Theorem xpeq1d 5012
Description: Equality deduction for Cartesian product. (Contributed by Jeff Madsen, 17-Jun-2010.)
Hypothesis
Ref Expression
xpeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
xpeq1d  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  C ) )

Proof of Theorem xpeq1d
StepHypRef Expression
1 xpeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 xpeq1 5003 . 2  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    X. cxp 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-opab 4496  df-xp 4995
This theorem is referenced by:  csbres  5266  xpssres  5298  curry1  6877  fparlem3  6887  fparlem4  6888  ixpsnf1o  7511  xpfi  7793  dfac5lem3  8509  dfac5lem4  8510  cdaassen  8565  hashxplem  12473  repsw1  12737  subgga  16317  gasubg  16319  sylow2blem2  16620  psrval  17990  mpfrcl  18166  evlsval  18167  mamufval  18865  mat1dimscm  18955  mdetunilem3  19094  mdetunilem4  19095  mdetunilem9  19100  txindislem  20112  txtube  20119  txcmplem1  20120  txhaus  20126  xkoinjcn  20166  pt1hmeo  20285  tsmsxplem1  20633  tsmsxplem2  20634  cnmpt2pc  21406  dchrval  23487  axlowdimlem15  24237  axlowdim  24242  0ofval  25680  esumcvg  28070  sxbrsigalem0  28220  sxbrsigalem3  28221  sxbrsigalem2  28235  ofcccat  28476  mexval2  28841  sdclem1  30212  ismrer1  30310  mzpclval  30633  mendval  31108  ldualset  34725  dibval  36744  dibval3N  36748  dib0  36766  dihwN  36891  hdmap1fval  37399
  Copyright terms: Public domain W3C validator