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

Theorem mpt2eq3dv 6674
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
mpt2eq3dv.1 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
mpt2eq3dv (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)

Proof of Theorem mpt2eq3dv
StepHypRef Expression
1 mpt2eq3dv.1 . . 3 (𝜑𝐶 = 𝐷)
213ad2ant1 1080 . 2 ((𝜑𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpt2eq3dva 6672 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  cmpt2 6606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-oprab 6608  df-mpt2 6609
This theorem is referenced by:  seqomeq12  7494  cantnfval  8509  seqeq2  12745  seqeq3  12746  relexpsucnnr  13699  lsmfval  17974  phssip  19922  mamuval  20111  matsc  20175  marrepval0  20286  marrepval  20287  marepvval0  20291  marepvval  20292  submaval0  20305  mdetr0  20330  mdet0  20331  mdetunilem7  20343  mdetunilem8  20344  madufval  20362  maduval  20363  maducoeval2  20365  madutpos  20367  madugsum  20368  madurid  20369  minmar1val0  20372  minmar1val  20373  pmat0opsc  20422  pmat1opsc  20423  mat2pmatval  20448  cpm2mval  20474  decpmatid  20494  pmatcollpw2lem  20501  pmatcollpw3lem  20507  mply1topmatval  20528  mp2pm2mplem1  20530  mp2pm2mplem4  20533  ttgval  25655  smatfval  29640  ofceq  29937  finxpeq1  32852  matunitlindflem1  33034  idfusubc  41151  digfval  41680
  Copyright terms: Public domain W3C validator