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

Theorem mpt2eq3dv 6340
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 1012 . 2  |-  ( (
ph  /\  x  e.  A  /\  y  e.  B
)  ->  C  =  D )
32mpt2eq3dva 6338 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 1374    e. wcel 1762    |-> cmpt2 6279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-oprab 6281  df-mpt2 6282
This theorem is referenced by:  cantnfval  8078  matsc  18714  marrepval0  18825  marrepval  18826  marepvval0  18830  marepvval  18831  submaval0  18844  mdetr0  18869  mdet0  18870  mdetunilem7  18882  mdetunilem8  18883  maducoeval2  18904  madutpos  18906  madugsum  18907  madurid  18908  minmar1val0  18911  minmar1val  18912  pmat0opsc  18961  pmat1opsc  18962  mat2pmatval  18987  cpm2mval  19013  decpmatid  19033  pmatcollpw2lem  19040  pmatcollpw3lem  19046  mply1topmatval  19067  mp2pm2mplem1  19069  mp2pm2mplem4  19072
  Copyright terms: Public domain W3C validator