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

Theorem xpeq1d 5552
 Description: Equality deduction for Cartesian product. (Contributed by Jeff Madsen, 17-Jun-2010.)
Hypothesis
Ref Expression
xpeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
xpeq1d (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Proof of Theorem xpeq1d
StepHypRef Expression
1 xpeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 xpeq1 5537 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
31, 2syl 17 1 (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   × cxp 5521 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-opab 5097  df-xp 5529 This theorem is referenced by:  csbres  5825  xpssres  5859  curry1  7795  fparlem3  7805  fparlem4  7806  ixpsnf1o  8503  xpfi  8791  dfac5lem3  9554  dfac5lem4  9555  hashxplem  13810  repsw1  14156  subgga  18443  gasubg  18445  sylow2blem2  18759  psrval  20623  mpfrcl  20794  evlsval  20795  mamufval  21033  mat1dimscm  21121  mdetunilem3  21260  mdetunilem4  21261  mdetunilem9  21266  txindislem  22279  txtube  22286  txcmplem1  22287  txhaus  22293  xkoinjcn  22333  pt1hmeo  22452  tsmsxplem1  22799  tsmsxplem2  22800  cnmpopc  23574  dchrval  25862  axlowdimlem15  26794  axlowdim  26799  0ofval  28614  hashxpe  30599  esumcvg  31521  sxbrsigalem0  31705  sxbrsigalem3  31706  sxbrsigalem2  31720  ofcccat  31989  lpadval  32123  lpadlem3  32125  mexval2  32929  csbfinxpg  34956  poimirlem1  35209  poimirlem2  35210  poimirlem3  35211  poimirlem4  35212  poimirlem5  35213  poimirlem6  35214  poimirlem7  35215  poimirlem8  35216  poimirlem10  35218  poimirlem11  35219  poimirlem12  35220  poimirlem15  35223  poimirlem16  35224  poimirlem17  35225  poimirlem18  35226  poimirlem19  35227  poimirlem20  35228  poimirlem21  35229  poimirlem22  35230  poimirlem23  35231  poimirlem24  35232  poimirlem26  35234  poimirlem27  35235  poimirlem28  35236  poimirlem32  35240  sdclem1  35332  ismrer1  35427  ldualset  36572  dibval  38589  dibval3N  38593  dib0  38611  dihwN  38736  hdmap1fval  39243  fsuppssind  39627  mzpclval  39837  mendval  40298
 Copyright terms: Public domain W3C validator