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

Theorem xpeq1d 4970
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 4961 . 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 1370    X. cxp 4945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-opab 4458  df-xp 4953
This theorem is referenced by:  csbres  5220  xpssres  5251  curry1  6773  fparlem3  6783  fparlem4  6784  ixpsnf1o  7412  xpfi  7693  dfac5lem3  8405  dfac5lem4  8406  cdaassen  8461  hashxplem  12312  repsw1  12538  subgga  15936  gasubg  15938  sylow2blem2  16240  psrval  17551  mpfrcl  17727  evlsval  17728  mamufval  18407  mdetunilem3  18551  mdetunilem4  18552  mdetunilem9  18557  txindislem  19337  txtube  19344  txcmplem1  19345  txhaus  19351  xkoinjcn  19391  pt1hmeo  19510  tsmsxplem1  19858  tsmsxplem2  19859  cnmpt2pc  20631  dchrval  22705  axlowdimlem15  23353  axlowdim  23358  0ofval  24338  esumcvg  26679  sxbrsigalem0  26829  sxbrsigalem3  26830  sxbrsigalem2  26844  ofcccat  27085  sdclem1  28786  ismrer1  28884  mzpclval  29208  mendval  29687  mat1dimscm  31036  ldualset  33093  dibval  35110  dibval3N  35114  dib0  35132  dihwN  35257  hdmap1fval  35765
  Copyright terms: Public domain W3C validator