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

Theorem mpteq1 4475
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 2453 . . 3  |-  ( x  e.  A  ->  C  =  C )
21rgen 2893 . 2  |-  A. x  e.  A  C  =  C
3 mpteq12 4474 . 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 1370    e. wcel 1758   A.wral 2796    |-> cmpt 4453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-ral 2801  df-opab 4454  df-mpt 4455
This theorem is referenced by:  mpteq1d  4476  fmptap  6005  mpt2mpt  6287  mpt2mptsx  6742  mpt2mpts  6743  tposf12  6875  oarec  7106  pwfseq  8937  wunex2  9011  wuncval2  9020  swrdlend  12438  vrmdfval  15648  pmtrfval  16070  sylow1  16218  sylow2b  16238  sylow3lem5  16246  sylow3  16248  gsumconst  16544  gsum2dlem2  16579  gsum2dOLD  16581  gsumcom2  16584  srgbinomlem4  16759  mvrfval  17612  mplcoe1  17663  mplcoe5  17667  mplcoe2OLD  17669  evlsval  17724  ply1coe  17866  ply1coeOLD  17867  evl1gsumd  17911  gsumfsum  17999  mavmul0  18485  m2detleiblem3  18562  m2detleiblem4  18563  madugsum  18576  cramer0  18623  restco  18895  cnmpt1t  19365  cnmpt2t  19373  fmval  19643  symgtgp  19799  prdstgpd  19822  dfarea  22482  istrkg2ld  23050  gsumvsca1  26391  gsumvsca2  26392  indv  26609  gsumesum  26650  esumlub  26651  sitg0  26871  sdclem2  28781  stoweidlem9  29947  wrd2f1tovbij  30398  wlknwwlknbij2  30489  wlkiswwlkbij2  30496  wwlkextbij  30508  coe1fzgsumd  30986  pmatcollpw3fi1lem1  31254  cpmadumatpolylem1  31348  chcoeffeqlem  31353
  Copyright terms: Public domain W3C validator