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

Theorem mpt2eq3dv 6955
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 1164 . 2 ((𝜑𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpt2eq3dva 6953 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1653  wcel 2157  cmpt2 6880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-oprab 6882  df-mpt2 6883
This theorem is referenced by:  seqomeq12  7788  cantnfval  8815  seqeq2  13059  seqeq3  13060  relexpsucnnr  14106  lsmfval  18366  phssip  20327  mamuval  20517  matsc  20582  marrepval0  20693  marrepval  20694  marepvval0  20698  marepvval  20699  submaval0  20712  mdetr0  20737  mdet0  20738  mdetunilem7  20750  mdetunilem8  20751  madufval  20769  maduval  20770  maducoeval2  20772  madutpos  20774  madugsum  20775  madurid  20776  minmar1val0  20779  minmar1val  20780  pmat0opsc  20831  pmat1opsc  20832  mat2pmatval  20857  cpm2mval  20883  decpmatid  20903  pmatcollpw2lem  20910  pmatcollpw3lem  20916  mply1topmatval  20937  mp2pm2mplem1  20939  mp2pm2mplem4  20942  ttgval  26112  smatfval  30377  ofceq  30675  reprval  31208  finxpeq1  33721  matunitlindflem1  33894  idfusubc  42665  digfval  43190
  Copyright terms: Public domain W3C validator