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

Theorem mpt2eq3dv 6348
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 1018 . 2  |-  ( (
ph  /\  x  e.  A  /\  y  e.  B
)  ->  C  =  D )
32mpt2eq3dva 6346 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 1383    e. wcel 1804    |-> cmpt2 6283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-oprab 6285  df-mpt2 6286
This theorem is referenced by:  seqomeq12  7121  cantnfval  8090  seqeq2  12090  seqeq3  12091  lsmfval  16532  mamuval  18761  matsc  18825  marrepval0  18936  marrepval  18937  marepvval0  18941  marepvval  18942  submaval0  18955  mdetr0  18980  mdet0  18981  mdetunilem7  18993  mdetunilem8  18994  madufval  19012  maduval  19013  maducoeval2  19015  madutpos  19017  madugsum  19018  madurid  19019  minmar1val0  19022  minmar1val  19023  pmat0opsc  19072  pmat1opsc  19073  mat2pmatval  19098  cpm2mval  19124  decpmatid  19144  pmatcollpw2lem  19151  pmatcollpw3lem  19157  mply1topmatval  19178  mp2pm2mplem1  19180  mp2pm2mplem4  19183  ttgval  24050  ofceq  27969  relexp0  28925  relexpsucr  28926  idfusubc  32399
  Copyright terms: Public domain W3C validator