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

Theorem xpeq1d 5022
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 5013 . 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 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:  csbres  5274  xpssres  5306  curry1  6872  fparlem3  6882  fparlem4  6883  ixpsnf1o  7506  xpfi  7787  dfac5lem3  8502  dfac5lem4  8503  cdaassen  8558  hashxplem  12451  repsw1  12712  subgga  16130  gasubg  16132  sylow2blem2  16434  psrval  17779  mpfrcl  17955  evlsval  17956  mamufval  18651  mat1dimscm  18741  mdetunilem3  18880  mdetunilem4  18881  mdetunilem9  18886  txindislem  19866  txtube  19873  txcmplem1  19874  txhaus  19880  xkoinjcn  19920  pt1hmeo  20039  tsmsxplem1  20387  tsmsxplem2  20388  cnmpt2pc  21160  dchrval  23234  axlowdimlem15  23932  axlowdim  23937  0ofval  25375  esumcvg  27729  sxbrsigalem0  27879  sxbrsigalem3  27880  sxbrsigalem2  27894  ofcccat  28135  sdclem1  29837  ismrer1  29935  mzpclval  30259  mendval  30737  ldualset  33922  dibval  35939  dibval3N  35943  dib0  35961  dihwN  36086  hdmap1fval  36594
  Copyright terms: Public domain W3C validator