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

Theorem mpteq1 4497
Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Assertion
Ref Expression
mpteq1  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    C( x)

Proof of Theorem mpteq1
StepHypRef Expression
1 eqidd 2421 . . 3  |-  ( x  e.  A  ->  C  =  C )
21rgen 2783 . 2  |-  A. x  e.  A  C  =  C
3 mpteq12 4496 . 2  |-  ( ( A  =  B  /\  A. x  e.  A  C  =  C )  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
42, 3mpan2 675 1  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1867   A.wral 2773    |-> cmpt 4475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-ral 2778  df-opab 4476  df-mpt 4477
This theorem is referenced by:  mpteq1d  4498  fmptap  6093  mpt2mpt  6393  mpt2mptsx  6861  mpt2mpts  6862  tposf12  6997  oarec  7262  pwfseq  9078  wunex2  9152  wuncval2  9161  wrd2f1tovbij  13003  vrmdfval  16584  pmtrfval  17035  sylow1  17183  sylow2b  17203  sylow3lem5  17211  sylow3  17213  gsumconst  17495  gsum2dlem2  17531  gsumcom2  17535  srgbinomlem4  17704  mvrfval  18572  mplcoe1  18617  mplcoe5  18620  evlsval  18670  ply1coe  18817  ply1coeOLD  18818  coe1fzgsumd  18824  evls1fval  18836  evl1gsumd  18873  gsumfsum  18962  mavmul0  19501  m2detleiblem3  19578  m2detleiblem4  19579  madugsum  19592  cramer0  19639  pmatcollpw3fi1lem1  19734  restco  20104  cnmpt1t  20604  cnmpt2t  20612  fmval  20882  symgtgp  21040  prdstgpd  21063  dfarea  23748  istrkg2ld  24368  wlknwwlknbij2  25284  wlkiswwlkbij2  25291  wwlkextbij  25303  gsumvsca1  28381  gsumvsca2  28382  indv  28670  gsumesum  28716  esumlub  28717  esum2d  28750  sitg0  29004  sdclem2  31775  mpteq1i  37079  stoweidlem9  37442  sge0sn  37759  sge0iunmptlemfi  37793  usgedgleord  38502  usgedgleordALT  38503
  Copyright terms: Public domain W3C validator