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

Theorem mpoeq3dv 7222
 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 1130 . 2 ((𝜑𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpoeq3dva 7220 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111   ∈ cmpo 7147 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-oprab 7149  df-mpo 7150 This theorem is referenced by:  seqomeq12  8091  cantnfval  9133  seqeq2  13388  seqeq3  13389  relexpsucnnr  14396  lsmfval  18776  phssip  20369  mamuval  21034  matsc  21096  marrepval0  21207  marrepval  21208  marepvval0  21212  marepvval  21213  submaval0  21226  mdetr0  21251  mdet0  21252  mdetunilem7  21264  mdetunilem8  21265  madufval  21283  maduval  21284  maducoeval2  21286  madutpos  21288  madugsum  21289  madurid  21290  minmar1val0  21293  minmar1val  21294  pmat0opsc  21344  pmat1opsc  21345  mat2pmatval  21370  cpm2mval  21396  decpmatid  21416  pmatcollpw2lem  21423  pmatcollpw3lem  21429  mply1topmatval  21450  mp2pm2mplem1  21452  mp2pm2mplem4  21455  ttgval  26713  smatfval  31214  ofceq  31532  reprval  32057  finxpeq1  34954  matunitlindflem1  35204  mnringmulrvald  41106  idfusubc  44658  digfval  45177  2arymaptfv  45231  itcoval  45241
 Copyright terms: Public domain W3C validator