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

Theorem xpeq12d 4972
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 4966 . 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 1370    X. cxp 4945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-opab 4458  df-xp 4953
This theorem is referenced by:  opeliunxp  4997  xpcoid  5485  mpt2mptsx  6746  dmmpt2ssx  6748  fmpt2x  6749  ovmptss  6763  fparlem3  6783  fparlem4  6784  erssxp  7233  marypha2lem2  7796  hartogslem1  7866  ackbij1lem8  8506  r1om  8523  fictb  8524  isfin6  8579  axcc2lem  8715  axcc2  8716  axdc4lem  8734  fpwwe2cbv  8907  fpwwe2lem2  8909  fpwwe2lem3  8910  fpwwe2lem8  8914  fpwwe2lem12  8918  fpwwe2lem13  8919  fpwwe2  8920  fpwwecbv  8921  fpwwelem  8922  canthwelem  8927  canthwe  8928  pwfseqlem4  8939  fsum2dlem  13354  fsumcom2  13358  ackbijnn  13408  prdsval  14511  imasval  14567  imasaddfnlem  14584  comfffval  14755  comfeq  14763  oppcval  14770  sscfn1  14848  sscfn2  14849  isssc  14851  ssceq  14857  reschomf  14862  isfunc  14892  idfuval  14904  funcres  14924  funcpropd  14928  fucval  14986  fucpropd  15005  homafval  15015  homaval  15017  setcval  15063  catcval  15082  xpcval  15105  xpchom  15108  xpchom2  15114  1stfval  15119  2ndfval  15122  xpcpropd  15136  evlfval  15145  hofval  15180  hofpropd  15195  islat  15335  istsr  15505  cnvtsr  15510  isdir  15520  tsrdir  15526  frmdval  15647  isga  15927  symgval  16002  gsumcom2  16588  gsumxp  16589  gsumxpOLD  16591  ablfaclem3  16709  psrval  17551  opsrval  17679  mamufval  18407  mamudm  18412  matval  18435  mvmulfval  18479  mavmuldm  18487  mavmul0g  18490  txbas  19271  ptbasfi  19285  txindis  19338  ustval  19908  trust  19935  utop2nei  19956  utop3cls  19957  utopreg  19958  ussval  19965  ressuss  19969  tususs  19976  fmucnd  19998  cfilufg  19999  trcfilu  20000  neipcfilu  20002  ispsmet  20011  prdsdsf  20073  prdsxmet  20075  ressprdsds  20077  xpsdsfn2  20084  xpsxmetlem  20085  xpsmet  20088  isxms  20153  isms  20155  xmspropd  20179  mspropd  20180  setsxms  20185  setsms  20186  imasf1oxms  20195  imasf1oms  20196  ressxms  20231  ressms  20232  prdsxmslem2  20235  tmsxps  20242  metuvalOLD  20255  metuval  20256  metustexhalfOLD  20269  metustexhalf  20270  nmpropd2  20318  ngppropd  20354  tngngp2  20369  pi1addf  20750  pi1addval  20751  iscms  20987  cmspropd  20991  cmsss  20992  cmetcusp  20997  rrxds  21028  rrxmfval  21036  minveclem3a  21045  dvlip2  21599  dchrval  22705  brcgr  23297  isgrp2d  23873  isgrpda  23935  efghgrp  24011  isrngo  24016  isrngod  24017  rngosn3  24064  isdivrngo  24069  issh  24761  prsssdm  26491  ordtrestNEW  26495  ordtrest2NEW  26497  isrrext  26573  sibfof  26869  cvmliftlem15  27330  fprod2dlem  27634  fprodcom2  27638  funtransport  28205  fvtransport  28206  filnetlem4  28749  prdsbnd2  28841  cnpwstotbnd  28843  heiborlem3  28859  aomclem8  29561  is2wlkonot  30529  is2spthonot  30530  2wlksot  30533  2spthsot  30534  2wlkonot3v  30541  2spthonot3v  30542  opeliun2xp  30867  dmmpt2ssx2  30874  bj-diagval  32848  ldualset  33093  dvhfset  35048  dvhset  35049  dibffval  35108  dibfval  35109  hdmap1fval  35765
  Copyright terms: Public domain W3C validator