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

Theorem mpt2eq3dv 6763
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 1102 . 2 ((𝜑𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
32mpt2eq3dva 6761 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  cmpt2 6692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-oprab 6694  df-mpt2 6695
This theorem is referenced by:  seqomeq12  7594  cantnfval  8603  seqeq2  12845  seqeq3  12846  relexpsucnnr  13809  lsmfval  18099  phssip  20051  mamuval  20240  matsc  20304  marrepval0  20415  marrepval  20416  marepvval0  20420  marepvval  20421  submaval0  20434  mdetr0  20459  mdet0  20460  mdetunilem7  20472  mdetunilem8  20473  madufval  20491  maduval  20492  maducoeval2  20494  madutpos  20496  madugsum  20497  madurid  20498  minmar1val0  20501  minmar1val  20502  pmat0opsc  20551  pmat1opsc  20552  mat2pmatval  20577  cpm2mval  20603  decpmatid  20623  pmatcollpw2lem  20630  pmatcollpw3lem  20636  mply1topmatval  20657  mp2pm2mplem1  20659  mp2pm2mplem4  20662  ttgval  25800  smatfval  29989  ofceq  30287  reprval  30816  finxpeq1  33353  matunitlindflem1  33535  idfusubc  42191  digfval  42716
  Copyright terms: Public domain W3C validator