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

Theorem xpeq12d 4852
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 4846 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )
41, 2, 3syl2anc 654 1  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    X. cxp 4825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-opab 4339  df-xp 4833
This theorem is referenced by:  opeliunxp  4877  xpcoid  5366  mpt2mptsx  6626  dmmpt2ssx  6628  fmpt2x  6629  ovmptss  6643  fparlem3  6663  fparlem4  6664  erssxp  7112  marypha2lem2  7674  hartogslem1  7744  ackbij1lem8  8384  r1om  8401  fictb  8402  isfin6  8457  axcc2lem  8593  axcc2  8594  axdc4lem  8612  fpwwe2cbv  8785  fpwwe2lem2  8787  fpwwe2lem3  8788  fpwwe2lem8  8792  fpwwe2lem12  8796  fpwwe2lem13  8797  fpwwe2  8798  fpwwecbv  8799  fpwwelem  8800  canthwelem  8805  canthwe  8806  pwfseqlem4  8817  fsum2dlem  13221  fsumcom2  13225  ackbijnn  13274  prdsval  14376  imasval  14432  imasaddfnlem  14449  comfffval  14620  comfeq  14628  oppcval  14635  sscfn1  14713  sscfn2  14714  isssc  14716  ssceq  14722  reschomf  14727  isfunc  14757  idfuval  14769  funcres  14789  funcpropd  14793  fucval  14851  fucpropd  14870  homafval  14880  homaval  14882  setcval  14928  catcval  14947  xpcval  14970  xpchom  14973  xpchom2  14979  1stfval  14984  2ndfval  14987  xpcpropd  15001  evlfval  15010  hofval  15045  hofpropd  15060  islat  15200  istsr  15370  cnvtsr  15375  isdir  15385  tsrdir  15391  frmdval  15509  isga  15789  symgval  15864  gsumcom2  16441  gsumxp  16442  gsumxpOLD  16444  ablfaclem3  16562  psrval  17363  opsrval  17488  mamufval  18125  mamudm  18130  matval  18153  mvmulfval  18195  mavmuldm  18203  mavmul0g  18206  txbas  18982  ptbasfi  18996  txindis  19049  ustval  19619  trust  19646  utop2nei  19667  utop3cls  19668  utopreg  19669  ussval  19676  ressuss  19680  tususs  19687  fmucnd  19709  cfilufg  19710  trcfilu  19711  neipcfilu  19713  ispsmet  19722  prdsdsf  19784  prdsxmet  19786  ressprdsds  19788  xpsdsfn2  19795  xpsxmetlem  19796  xpsmet  19799  isxms  19864  isms  19866  xmspropd  19890  mspropd  19891  setsxms  19896  setsms  19897  imasf1oxms  19906  imasf1oms  19907  ressxms  19942  ressms  19943  prdsxmslem2  19946  tmsxps  19953  metuvalOLD  19966  metuval  19967  metustexhalfOLD  19980  metustexhalf  19981  nmpropd2  20029  ngppropd  20065  tngngp2  20080  pi1addf  20461  pi1addval  20462  iscms  20698  cmspropd  20702  cmsss  20703  cmetcusp  20708  rrxds  20739  rrxmfval  20747  minveclem3a  20756  dvlip2  21309  dchrval  22458  brcgr  22969  isgrp2d  23545  isgrpda  23607  efghgrp  23683  isrngo  23688  isrngod  23689  rngosn3  23736  isdivrngo  23741  issh  24433  prsssdm  26201  ordtrestNEW  26205  ordtrest2NEW  26207  isrrext  26283  sibfof  26574  cvmliftlem15  27035  fprod2dlem  27338  fprodcom2  27342  funtransport  27909  fvtransport  27910  filnetlem4  28446  prdsbnd2  28538  cnpwstotbnd  28540  heiborlem3  28556  aomclem8  29259  is2wlkonot  30228  is2spthonot  30229  2wlksot  30232  2spthsot  30233  2wlkonot3v  30240  2spthonot3v  30241  opeliun2xp  30565  dmmpt2ssx2  30572  bj-diagval  32126  ldualset  32364  dvhfset  34319  dvhset  34320  dibffval  34379  dibfval  34380  hdmap1fval  35036
  Copyright terms: Public domain W3C validator