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

Theorem mpteq1 4517
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 2444 . . 3  |-  ( x  e.  A  ->  C  =  C )
21rgen 2803 . 2  |-  A. x  e.  A  C  =  C
3 mpteq12 4516 . 2  |-  ( ( A  =  B  /\  A. x  e.  A  C  =  C )  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
42, 3mpan2 671 1  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804   A.wral 2793    |-> cmpt 4495
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-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ral 2798  df-opab 4496  df-mpt 4497
This theorem is referenced by:  mpteq1d  4518  fmptap  6079  mpt2mpt  6379  mpt2mptsx  6848  mpt2mpts  6849  tposf12  6982  oarec  7213  pwfseq  9045  wunex2  9119  wuncval2  9128  wrd2f1tovbij  12880  vrmdfval  16003  pmtrfval  16454  sylow1  16602  sylow2b  16622  sylow3lem5  16630  sylow3  16632  gsumconst  16933  gsum2dlem2  16977  gsum2dOLD  16979  gsumcom2  16982  srgbinomlem4  17173  mvrfval  18055  mplcoe1  18106  mplcoe5  18110  mplcoe2OLD  18112  evlsval  18167  ply1coe  18316  ply1coeOLD  18317  coe1fzgsumd  18323  evls1fval  18335  evl1gsumd  18372  gsumfsum  18463  mavmul0  19032  m2detleiblem3  19109  m2detleiblem4  19110  madugsum  19123  cramer0  19170  pmatcollpw3fi1lem1  19265  restco  19643  cnmpt1t  20144  cnmpt2t  20152  fmval  20422  symgtgp  20578  prdstgpd  20601  dfarea  23268  istrkg2ld  23836  wlknwwlknbij2  24692  wlkiswwlkbij2  24699  wwlkextbij  24711  gsumvsca1  27751  gsumvsca2  27752  indv  28004  gsumesum  28045  esumlub  28046  sitg0  28266  sdclem2  30211  stoweidlem9  31745  usgedgleord  32373  usgedgleordALT  32374
  Copyright terms: Public domain W3C validator