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

Theorem mpteq1 4292
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 2439 . . 3  |-  ( x  e.  A  ->  C  =  C )
21rgen 2773 . 2  |-  A. x  e.  A  C  =  C
3 mpteq12 4291 . 2  |-  ( ( A  =  B  /\  A. x  e.  A  C  =  C )  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
42, 3mpan2 654 1  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726   A.wral 2707    e. cmpt 4269
This theorem is referenced by:  mpteq1d  4293  fmptap  5926  mpt2mpt  6168  mpt2mptsx  6417  mpt2mpts  6418  tposf12  6507  oarec  6808  pwfseq  8544  wunex2  8618  wuncval2  8627  vrmdfval  14806  sylow1  15242  sylow2b  15262  sylow3lem5  15270  sylow3  15272  gsumconst  15537  gsum2d  15551  gsumcom2  15554  mvrfval  16489  mplcoe1  16533  mplcoe2  16535  ply1coe  16689  gsumfsum  16771  restco  17233  cnmpt1t  17702  cnmpt2t  17710  fmval  17980  symgtgp  18136  prdstgpd  18159  evlsval  19945  dfarea  20804  indv  24415  gsumesum  24456  esumlub  24457  sdclem2  26460  pmtrfval  27384  stoweidlem9  27748  swrdltnd  28215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2712  df-opab 4270  df-mpt 4271
  Copyright terms: Public domain W3C validator