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

Theorem xpeq1d 4852
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 4843 . 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 1364    X. cxp 4827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-clel 2431  df-opab 4341  df-xp 4835
This theorem is referenced by:  csbres  5102  xpssres  5134  curry1  6655  fparlem3  6665  fparlem4  6666  ixpsnf1o  7293  xpfi  7573  dfac5lem3  8285  dfac5lem4  8286  cdaassen  8341  hashxplem  12181  repsw1  12407  subgga  15800  gasubg  15802  sylow2blem2  16102  psrval  17365  mamufval  18127  mdetunilem3  18264  mdetunilem4  18265  mdetunilem9  18270  txindislem  19050  txtube  19057  txcmplem1  19058  txhaus  19064  xkoinjcn  19104  pt1hmeo  19223  tsmsxplem1  19571  tsmsxplem2  19572  cnmpt2pc  20344  mpfrcl  21372  evlsval  21373  dchrval  22460  axlowdimlem15  23027  axlowdim  23032  0ofval  24012  esumcvg  26391  sxbrsigalem0  26542  sxbrsigalem3  26543  sxbrsigalem2  26557  ofcccat  26792  sdclem1  28485  ismrer1  28583  mzpclval  28908  mendval  29387  mat1dimscm  30662  ldualset  32383  dibval  34400  dibval3N  34404  dib0  34422  dihwN  34547  hdmap1fval  35055
  Copyright terms: Public domain W3C validator