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

Theorem xpeq1d 4858
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 4849 . 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 1369    X. cxp 4833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-opab 4346  df-xp 4841
This theorem is referenced by:  csbres  5108  xpssres  5139  curry1  6659  fparlem3  6669  fparlem4  6670  ixpsnf1o  7295  xpfi  7575  dfac5lem3  8287  dfac5lem4  8288  cdaassen  8343  hashxplem  12187  repsw1  12413  subgga  15809  gasubg  15811  sylow2blem2  16111  psrval  17406  mpfrcl  17579  evlsval  17580  mamufval  18258  mdetunilem3  18395  mdetunilem4  18396  mdetunilem9  18401  txindislem  19181  txtube  19188  txcmplem1  19189  txhaus  19195  xkoinjcn  19235  pt1hmeo  19354  tsmsxplem1  19702  tsmsxplem2  19703  cnmpt2pc  20475  dchrval  22548  axlowdimlem15  23153  axlowdim  23158  0ofval  24138  esumcvg  26487  sxbrsigalem0  26638  sxbrsigalem3  26639  sxbrsigalem2  26653  ofcccat  26894  sdclem1  28592  ismrer1  28690  mzpclval  29014  mendval  29493  mat1dimscm  30794  ldualset  32610  dibval  34627  dibval3N  34631  dib0  34649  dihwN  34774  hdmap1fval  35282
  Copyright terms: Public domain W3C validator