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

Theorem xpeq1d 4936
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 4927 . 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 1399    X. cxp 4911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-opab 4426  df-xp 4919
This theorem is referenced by:  csbres  5189  xpssres  5220  curry1  6791  fparlem3  6801  fparlem4  6802  ixpsnf1o  7428  xpfi  7706  dfac5lem3  8419  dfac5lem4  8420  cdaassen  8475  hashxplem  12395  repsw1  12666  subgga  16455  gasubg  16457  sylow2blem2  16758  psrval  18124  mpfrcl  18300  evlsval  18301  mamufval  18972  mat1dimscm  19062  mdetunilem3  19201  mdetunilem4  19202  mdetunilem9  19207  txindislem  20219  txtube  20226  txcmplem1  20227  txhaus  20233  xkoinjcn  20273  pt1hmeo  20392  tsmsxplem1  20740  tsmsxplem2  20741  cnmpt2pc  21513  dchrval  23626  axlowdimlem15  24380  axlowdim  24385  0ofval  25819  esumcvg  28234  sxbrsigalem0  28398  sxbrsigalem3  28399  sxbrsigalem2  28413  ofcccat  28681  mexval2  29052  sdclem1  30402  ismrer1  30500  mzpclval  30823  mendval  31300  ldualset  35263  dibval  37282  dibval3N  37286  dib0  37304  dihwN  37429  hdmap1fval  37937
  Copyright terms: Public domain W3C validator