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

Theorem mpt2eq3dv 6363
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:   ,   ,

Proof of Theorem mpt2eq3dv
StepHypRef Expression
1 mpt2eq3dv.1 . . 3
213ad2ant1 1017 . 2
32mpt2eq3dva 6361 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  e.cmpt2 6298
This theorem is referenced by:  seqomeq12  7138  cantnfval  8108  seqeq2  12111  seqeq3  12112  lsmfval  16658  mamuval  18888  matsc  18952  marrepval0  19063  marrepval  19064  marepvval0  19068  marepvval  19069  submaval0  19082  mdetr0  19107  mdet0  19108  mdetunilem7  19120  mdetunilem8  19121  madufval  19139  maduval  19140  maducoeval2  19142  madutpos  19144  madugsum  19145  madurid  19146  minmar1val0  19149  minmar1val  19150  pmat0opsc  19199  pmat1opsc  19200  mat2pmatval  19225  cpm2mval  19251  decpmatid  19271  pmatcollpw2lem  19278  pmatcollpw3lem  19284  mply1topmatval  19305  mp2pm2mplem1  19307  mp2pm2mplem4  19310  ttgval  24178  ofceq  28096  relexp0  29052  relexpsucr  29053  idfusubc  32592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-oprab 6300  df-mpt2 6301
  Copyright terms: Public domain W3C validator