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

Theorem mpteq1 4369
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 2442 . . 3  |-  ( x  e.  A  ->  C  =  C )
21rgen 2779 . 2  |-  A. x  e.  A  C  =  C
3 mpteq12 4368 . 2  |-  ( ( A  =  B  /\  A. x  e.  A  C  =  C )  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
42, 3mpan2 666 1  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364    e. wcel 1761   A.wral 2713    e. cmpt 4347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-ral 2718  df-opab 4348  df-mpt 4349
This theorem is referenced by:  mpteq1d  4370  fmptap  5898  mpt2mpt  6181  mpt2mptsx  6636  mpt2mpts  6637  tposf12  6769  oarec  6997  pwfseq  8827  wunex2  8901  wuncval2  8910  swrdlend  12321  vrmdfval  15527  pmtrfval  15949  sylow1  16095  sylow2b  16115  sylow3lem5  16123  sylow3  16125  gsumconst  16419  gsum2dlem2  16452  gsum2dOLD  16454  gsumcom2  16457  srgbinomlem4  16631  mvrfval  17483  mplcoe1  17534  mplcoe2  17537  mplcoe2OLD  17538  ply1coe  17699  gsumfsum  17779  mavmul0  18263  m2detleiblem3  18335  m2detleiblem4  18336  madugsum  18349  cramer0  18396  restco  18668  cnmpt1t  19138  cnmpt2t  19146  fmval  19416  symgtgp  19572  prdstgpd  19595  evlsval  21429  dfarea  22297  gsumvsca1  26170  gsumvsca2  26171  indv  26389  gsumesum  26430  esumlub  26431  sitg0  26646  sdclem2  28547  stoweidlem9  29713  wrd2f1tovbij  30164  wlknwwlknbij2  30255  wlkiswwlkbij2  30262  wwlkextbij  30274
  Copyright terms: Public domain W3C validator