MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpoeq3dv Structured version   Visualization version   GIF version

Theorem mpoeq3dv 7491
Description: An equality deduction for the maps-to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018.)
Hypothesis
Ref Expression
mpoeq3dv.1 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
mpoeq3dv (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)

Proof of Theorem mpoeq3dv
StepHypRef Expression
1 mpoeq3dv.1 . . 3 (𝜑𝐶 = 𝐷)
213ad2ant1 1132 . 2 ((𝜑𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpoeq3dva 7489 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2105  cmpo 7414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1088  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-oprab 7416  df-mpo 7417
This theorem is referenced by:  ofeqd  7676  seqomeq12  8460  cantnfval  9669  seqeq2  13977  seqeq3  13978  relexpsucnnr  14979  idfusubc  17857  lsmfval  19554  phssip  21520  mamuval  22207  matsc  22271  marrepval0  22382  marrepval  22383  marepvval0  22387  marepvval  22388  submaval0  22401  mdetr0  22426  mdet0  22427  mdetunilem7  22439  mdetunilem8  22440  madufval  22458  maduval  22459  maducoeval2  22461  madutpos  22463  madugsum  22464  madurid  22465  minmar1val0  22468  minmar1val  22469  pmat0opsc  22519  pmat1opsc  22520  mat2pmatval  22545  cpm2mval  22571  decpmatid  22591  pmatcollpw2lem  22598  pmatcollpw3lem  22604  mply1topmatval  22625  mp2pm2mplem1  22627  mp2pm2mplem4  22630  ttgval  28558  ttgvalOLD  28559  smatfval  33238  ofceq  33558  reprval  34085  finxpeq1  36730  matunitlindflem1  36947  mnringmulrvald  43448  digfval  47444  2arymaptfv  47498  itcoval  47508
  Copyright terms: Public domain W3C validator