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

Theorem xpeq1d 4874
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 4865 . 2  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
31, 2syl 17 1  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1438    X. cxp 4849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-opab 4481  df-xp 4857
This theorem is referenced by:  csbres  5125  xpssres  5156  curry1  6897  fparlem3  6907  fparlem4  6908  ixpsnf1o  7568  xpfi  7846  dfac5lem3  8558  dfac5lem4  8559  cdaassen  8614  hashxplem  12604  repsw1  12882  subgga  16947  gasubg  16949  sylow2blem2  17266  psrval  18579  mpfrcl  18734  evlsval  18735  mamufval  19402  mat1dimscm  19492  mdetunilem3  19631  mdetunilem4  19632  mdetunilem9  19637  txindislem  20640  txtube  20647  txcmplem1  20648  txhaus  20654  xkoinjcn  20694  pt1hmeo  20813  tsmsxplem1  21159  tsmsxplem2  21160  cnmpt2pc  21948  dchrval  24154  axlowdimlem15  24978  axlowdim  24983  0ofval  26420  esumcvg  28909  sxbrsigalem0  29095  sxbrsigalem3  29096  sxbrsigalem2  29110  ofcccat  29432  mexval2  30143  csbfinxpg  31738  poimirlem1  31899  poimirlem2  31900  poimirlem3  31901  poimirlem4  31902  poimirlem5  31903  poimirlem6  31904  poimirlem7  31905  poimirlem8  31906  poimirlem10  31908  poimirlem11  31909  poimirlem12  31910  poimirlem15  31913  poimirlem16  31914  poimirlem17  31915  poimirlem18  31916  poimirlem19  31917  poimirlem20  31918  poimirlem21  31919  poimirlem22  31920  poimirlem23  31921  poimirlem24  31922  poimirlem26  31924  poimirlem27  31925  poimirlem28  31926  poimirlem32  31930  sdclem1  32030  ismrer1  32128  ldualset  32654  dibval  34673  dibval3N  34677  dib0  34695  dihwN  34820  hdmap1fval  35328  mzpclval  35530  mendval  36013
  Copyright terms: Public domain W3C validator