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

Theorem mpoeq3dv 7094
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 1126 . 2 ((𝜑𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpoeq3dva 7092 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1522  wcel 2080  cmpo 7021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-9 2090  ax-12 2140  ax-ext 2768
This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1082  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-oprab 7023  df-mpo 7024
This theorem is referenced by:  seqomeq12  7944  cantnfval  8980  seqeq2  13223  seqeq3  13224  relexpsucnnr  14218  lsmfval  18493  phssip  20484  mamuval  20679  matsc  20743  marrepval0  20854  marrepval  20855  marepvval0  20859  marepvval  20860  submaval0  20873  mdetr0  20898  mdet0  20899  mdetunilem7  20911  mdetunilem8  20912  madufval  20930  maduval  20931  maducoeval2  20933  madutpos  20935  madugsum  20936  madurid  20937  minmar1val0  20940  minmar1val  20941  pmat0opsc  20990  pmat1opsc  20991  mat2pmatval  21016  cpm2mval  21042  decpmatid  21062  pmatcollpw2lem  21069  pmatcollpw3lem  21075  mply1topmatval  21096  mp2pm2mplem1  21098  mp2pm2mplem4  21101  ttgval  26344  smatfval  30667  ofceq  30965  reprval  31490  finxpeq1  34211  matunitlindflem1  34432  idfusubc  43629  digfval  44152
  Copyright terms: Public domain W3C validator