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

Theorem xpeq12d 4860
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 4854 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  X.  C
)  =  ( B  X.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    X. cxp 4833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-opab 4346  df-xp 4841
This theorem is referenced by:  opeliunxp  4885  xpcoid  5373  mpt2mptsx  6632  dmmpt2ssx  6634  fmpt2x  6635  ovmptss  6649  fparlem3  6669  fparlem4  6670  erssxp  7116  marypha2lem2  7678  hartogslem1  7748  ackbij1lem8  8388  r1om  8405  fictb  8406  isfin6  8461  axcc2lem  8597  axcc2  8598  axdc4lem  8616  fpwwe2cbv  8789  fpwwe2lem2  8791  fpwwe2lem3  8792  fpwwe2lem8  8796  fpwwe2lem12  8800  fpwwe2lem13  8801  fpwwe2  8802  fpwwecbv  8803  fpwwelem  8804  canthwelem  8809  canthwe  8810  pwfseqlem4  8821  fsum2dlem  13229  fsumcom2  13233  ackbijnn  13283  prdsval  14385  imasval  14441  imasaddfnlem  14458  comfffval  14629  comfeq  14637  oppcval  14644  sscfn1  14722  sscfn2  14723  isssc  14725  ssceq  14731  reschomf  14736  isfunc  14766  idfuval  14778  funcres  14798  funcpropd  14802  fucval  14860  fucpropd  14879  homafval  14889  homaval  14891  setcval  14937  catcval  14956  xpcval  14979  xpchom  14982  xpchom2  14988  1stfval  14993  2ndfval  14996  xpcpropd  15010  evlfval  15019  hofval  15054  hofpropd  15069  islat  15209  istsr  15379  cnvtsr  15384  isdir  15394  tsrdir  15400  frmdval  15520  isga  15800  symgval  15875  gsumcom2  16455  gsumxp  16456  gsumxpOLD  16458  ablfaclem3  16576  psrval  17406  opsrval  17531  mamufval  18258  mamudm  18263  matval  18286  mvmulfval  18328  mavmuldm  18336  mavmul0g  18339  txbas  19115  ptbasfi  19129  txindis  19182  ustval  19752  trust  19779  utop2nei  19800  utop3cls  19801  utopreg  19802  ussval  19809  ressuss  19813  tususs  19820  fmucnd  19842  cfilufg  19843  trcfilu  19844  neipcfilu  19846  ispsmet  19855  prdsdsf  19917  prdsxmet  19919  ressprdsds  19921  xpsdsfn2  19928  xpsxmetlem  19929  xpsmet  19932  isxms  19997  isms  19999  xmspropd  20023  mspropd  20024  setsxms  20029  setsms  20030  imasf1oxms  20039  imasf1oms  20040  ressxms  20075  ressms  20076  prdsxmslem2  20079  tmsxps  20086  metuvalOLD  20099  metuval  20100  metustexhalfOLD  20113  metustexhalf  20114  nmpropd2  20162  ngppropd  20198  tngngp2  20213  pi1addf  20594  pi1addval  20595  iscms  20831  cmspropd  20835  cmsss  20836  cmetcusp  20841  rrxds  20872  rrxmfval  20880  minveclem3a  20889  dvlip2  21442  dchrval  22548  brcgr  23097  isgrp2d  23673  isgrpda  23735  efghgrp  23811  isrngo  23816  isrngod  23817  rngosn3  23864  isdivrngo  23869  issh  24561  prsssdm  26299  ordtrestNEW  26303  ordtrest2NEW  26305  isrrext  26381  sibfof  26678  cvmliftlem15  27139  fprod2dlem  27442  fprodcom2  27446  funtransport  28013  fvtransport  28014  filnetlem4  28555  prdsbnd2  28647  cnpwstotbnd  28649  heiborlem3  28665  aomclem8  29367  is2wlkonot  30335  is2spthonot  30336  2wlksot  30339  2spthsot  30340  2wlkonot3v  30347  2spthonot3v  30348  opeliun2xp  30672  dmmpt2ssx2  30679  bj-diagval  32372  ldualset  32610  dvhfset  34565  dvhset  34566  dibffval  34625  dibfval  34626  hdmap1fval  35282
  Copyright terms: Public domain W3C validator