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

Theorem mpoeq3dv 7512
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 1134 . 2 ((𝜑𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpoeq3dva 7510 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108  cmpo 7433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-oprab 7435  df-mpo 7436
This theorem is referenced by:  ofeqd  7699  seqomeq12  8494  cantnfval  9708  seqeq2  14046  seqeq3  14047  relexpsucnnr  15064  idfusubc  17945  lsmfval  19656  phssip  21676  mamuval  22397  matsc  22456  marrepval0  22567  marrepval  22568  marepvval0  22572  marepvval  22573  submaval0  22586  mdetr0  22611  mdet0  22612  mdetunilem7  22624  mdetunilem8  22625  madufval  22643  maduval  22644  maducoeval2  22646  madutpos  22648  madugsum  22649  madurid  22650  minmar1val0  22653  minmar1val  22654  pmat0opsc  22704  pmat1opsc  22705  mat2pmatval  22730  cpm2mval  22756  decpmatid  22776  pmatcollpw2lem  22783  pmatcollpw3lem  22789  mply1topmatval  22810  mp2pm2mplem1  22812  mp2pm2mplem4  22815  seqseq123d  28292  ttgval  28883  ttgvalOLD  28884  smatfval  33794  ofceq  34098  reprval  34625  finxpeq1  37387  matunitlindflem1  37623  mnringmulrvald  44246  digfval  48518  2arymaptfv  48572  itcoval  48582  dfswapf2  48967  postcofval  49059  precofval  49062  precofval2  49064
  Copyright terms: Public domain W3C validator