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

Theorem xpeq12d 4875
Description: Equality deduction for Cartesian product. (Contributed by NM, 8-Dec-2013.)
Hypotheses
Ref Expression
xpeq1d.1  |-  ( ph  ->  A  =  B )
xpeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
xpeq12d  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  D ) )

Proof of Theorem xpeq12d
StepHypRef Expression
1 xpeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 xpeq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 xpeq12 4869 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    X. cxp 4848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-opab 4480  df-xp 4856
This theorem is referenced by:  sqxpeqd  4876  opeliunxp  4902  mpt2mptsx  6867  dmmpt2ssx  6869  fmpt2x  6870  ovmptss  6885  fparlem3  6906  fparlem4  6907  erssxp  7391  marypha2lem2  7953  ackbij1lem8  8658  r1om  8675  fictb  8676  axcc2lem  8867  axcc2  8868  axdc4lem  8886  fsum2dlem  13819  fsumcom2  13823  ackbijnn  13874  fprod2dlem  14022  fprodcom2  14026  homaval  15914  xpcval  16050  xpchom  16053  xpchom2  16059  1stfval  16064  2ndfval  16067  xpcpropd  16081  evlfval  16090  isga  16933  symgval  17008  gsumcom2  17595  gsumxp  17596  ablfaclem3  17708  psrval  18574  mamufval  19397  mamudm  19400  mvmulfval  19554  mavmuldm  19562  mavmul0g  19565  txbas  20569  ptbasfi  20583  txindis  20636  tmsxps  21538  metustexhalf  21558  is2wlkonot  25577  is2spthonot  25578  2wlksot  25581  2spthsot  25582  2wlkonot3v  25589  2spthonot3v  25590  aciunf1lem  28254  esum2dlem  28909  cvmliftlem15  30017  mexval  30136  mpstval  30169  mclsval  30197  mclsax  30203  mclsppslem  30217  filnetlem4  31030  poimirlem26  31880  poimirlem28  31882  heiborlem3  32059  dvhfset  34567  dvhset  34568  dibffval  34627  dibfval  34628  hdmap1fval  35284  opeliun2xp  39388  dmmpt2ssx2  39392
  Copyright terms: Public domain W3C validator