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

Theorem mpt2eq3dv 6253
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 1009 . 2  |-  ( (
ph  /\  x  e.  A  /\  y  e.  B
)  ->  C  =  D )
32mpt2eq3dva 6251 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 1370    e. wcel 1758    |-> cmpt2 6194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-oprab 6196  df-mpt2 6197
This theorem is referenced by:  cantnfval  7979  matsc  18454  marrepval0  18485  marrepval  18486  marepvval0  18490  marepvval  18491  submaval0  18504  mdetr0  18529  mdet0  18530  mdetunilem7  18542  mdetunilem8  18543  maducoeval2  18564  madutpos  18566  madugsum  18567  madurid  18568  minmar1val0  18571  minmar1val  18572  pmat0opsc  31166  pmat1opsc  31167  mat2pmatval  31189  m2pminvval  31212  pmatcollpw1lem1  31225  pmatcollpw1id  31228  pmatcollpw1dst  31230  pmatcollpwlem  31235  pmatcollpw1aa0  31237  pmatcollpw4  31242  pmatcollpw4fi  31243  mply1topmatval  31253  pmattomply1ghmlem2  31256  pmattomply1f1lem  31257  pmattomply1rn  31259  pmattomply1coe1  31261  idpmattoidmply1  31262  mp2pm2mplem1  31263  mp2pm2mplem3  31265  mp2pm2mplem4  31266  mp2pm2mplem5  31267  mp2pm2mp  31268  pmattomply1fo  31270  pmattomply1ghm  31272  pmattomply1mhmlem2  31276  monmat2matmon  31280  cpmidgsum  31324  cpmadugsumfi  31333  chcoeffeq  31343  cayleyhamilton  31347  cayleyhamiltonALT  31348
  Copyright terms: Public domain W3C validator