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

Theorem xpeq12d 5024
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 5018 . 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 1379    X. cxp 4997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-opab 4506  df-xp 5005
This theorem is referenced by:  sqxpeqd  5025  opeliunxp  5051  mpt2mptsx  6847  dmmpt2ssx  6849  fmpt2x  6850  ovmptss  6864  fparlem3  6885  fparlem4  6886  erssxp  7334  marypha2lem2  7896  hartogslem1  7967  ackbij1lem8  8607  r1om  8624  fictb  8625  axcc2lem  8816  axcc2  8817  axdc4lem  8835  fpwwe2cbv  9008  fpwwe2lem2  9010  fpwwe2lem3  9011  fpwwe2lem8  9015  fpwwe2lem12  9019  fpwwe2lem13  9020  fpwwe2  9021  fpwwecbv  9022  fpwwelem  9023  canthwelem  9028  canthwe  9029  pwfseqlem4  9040  fsum2dlem  13548  fsumcom2  13552  ackbijnn  13603  prdsval  14710  imasval  14766  imasaddfnlem  14783  comfffval  14954  comfeq  14962  oppcval  14969  sscfn1  15047  sscfn2  15048  isssc  15050  ssceq  15056  reschomf  15061  isfunc  15091  idfuval  15103  funcres  15123  funcpropd  15127  fucval  15185  fucpropd  15204  homafval  15214  homaval  15216  setcval  15262  catcval  15281  xpcval  15304  xpchom  15307  xpchom2  15313  1stfval  15318  2ndfval  15321  xpcpropd  15335  evlfval  15344  hofval  15379  hofpropd  15394  cnvtsr  15709  tsrdir  15725  frmdval  15851  isga  16134  symgval  16209  gsumcom2  16806  gsumxp  16807  gsumxpOLD  16809  ablfaclem3  16940  psrval  17810  opsrval  17938  mamufval  18682  mamudm  18685  matval  18708  mvmulfval  18839  mavmuldm  18847  mavmul0g  18850  txbas  19831  ptbasfi  19845  txindis  19898  ustval  20468  trust  20495  utop2nei  20516  utop3cls  20517  utopreg  20518  ussval  20525  ressuss  20529  tususs  20536  fmucnd  20558  cfilufg  20559  trcfilu  20560  neipcfilu  20562  ispsmet  20571  prdsdsf  20633  prdsxmet  20635  ressprdsds  20637  xpsdsfn2  20644  xpsxmetlem  20645  xpsmet  20648  isxms  20713  isms  20715  xmspropd  20739  mspropd  20740  setsxms  20745  setsms  20746  imasf1oxms  20755  imasf1oms  20756  ressxms  20791  ressms  20792  prdsxmslem2  20795  tmsxps  20802  metuvalOLD  20815  metuval  20816  metustexhalfOLD  20829  metustexhalf  20830  nmpropd2  20878  ngppropd  20914  tngngp2  20929  pi1addf  21310  pi1addval  21311  iscms  21547  cmspropd  21551  cmsss  21552  cmetcusp  21557  rrxds  21588  rrxmfval  21596  minveclem3a  21605  dvlip2  22159  dchrval  23265  brcgr  23907  is2wlkonot  24567  is2spthonot  24568  2wlksot  24571  2spthsot  24572  2wlkonot3v  24579  2spthonot3v  24580  isgrp2d  24941  isgrpda  25003  efghgrp  25079  isrngo  25084  isrngod  25085  rngosn3  25132  isdivrngo  25137  issh  25829  prsssdm  27563  ordtrestNEW  27567  ordtrest2NEW  27569  isrrext  27645  qtophaus  27665  sibfof  27950  cvmliftlem15  28411  fprod2dlem  28715  fprodcom2  28719  funtransport  29286  fvtransport  29287  filnetlem4  29830  prdsbnd2  29922  cnpwstotbnd  29924  heiborlem3  29940  aomclem8  30639  mgmplusgiop  31961  opeliun2xp  32018  dmmpt2ssx2  32022  bj-diagval  33695  ldualset  33940  dvhfset  35895  dvhset  35896  dibffval  35955  dibfval  35956  hdmap1fval  36612
  Copyright terms: Public domain W3C validator