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

Theorem mpt2eq3dv 6336
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  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
mpt2eq3dv  |-  ( ph  ->  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A , 
y  e.  B  |->  D ) )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    A( x, y)    B( x, y)    C( x, y)    D( x, y)

Proof of Theorem mpt2eq3dv
StepHypRef Expression
1 mpt2eq3dv.1 . . 3  |-  ( ph  ->  C  =  D )
213ad2ant1 1015 . 2  |-  ( (
ph  /\  x  e.  A  /\  y  e.  B
)  ->  C  =  D )
32mpt2eq3dva 6334 1  |-  ( ph  ->  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A , 
y  e.  B  |->  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    e. wcel 1823    |-> cmpt2 6272
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-oprab 6274  df-mpt2 6275
This theorem is referenced by:  seqomeq12  7111  cantnfval  8078  seqeq2  12093  seqeq3  12094  relexpsucnnr  12942  lsmfval  16857  mamuval  19055  matsc  19119  marrepval0  19230  marrepval  19231  marepvval0  19235  marepvval  19236  submaval0  19249  mdetr0  19274  mdet0  19275  mdetunilem7  19287  mdetunilem8  19288  madufval  19306  maduval  19307  maducoeval2  19309  madutpos  19311  madugsum  19312  madurid  19313  minmar1val0  19316  minmar1val  19317  pmat0opsc  19366  pmat1opsc  19367  mat2pmatval  19392  cpm2mval  19418  decpmatid  19438  pmatcollpw2lem  19445  pmatcollpw3lem  19451  mply1topmatval  19472  mp2pm2mplem1  19474  mp2pm2mplem4  19477  ttgval  24380  ofceq  28326  idfusubc  32926  digfval  33472
  Copyright terms: Public domain W3C validator