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

Theorem mpteq1 4483
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 2452 . . 3  |-  ( x  e.  A  ->  C  =  C )
21rgen 2747 . 2  |-  A. x  e.  A  C  =  C
3 mpteq12 4482 . 2  |-  ( ( A  =  B  /\  A. x  e.  A  C  =  C )  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
42, 3mpan2 677 1  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444    e. wcel 1887   A.wral 2737    |-> cmpt 4461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-ral 2742  df-opab 4462  df-mpt 4463
This theorem is referenced by:  mpteq1d  4484  fmptap  6087  mpt2mpt  6388  mpt2mptsx  6856  mpt2mpts  6857  tposf12  6998  oarec  7263  pwfseq  9089  wunex2  9163  wuncval2  9172  wrd2f1tovbij  13035  vrmdfval  16640  pmtrfval  17091  sylow1  17255  sylow2b  17275  sylow3lem5  17283  sylow3  17285  gsumconst  17567  gsum2dlem2  17603  gsumcom2  17607  srgbinomlem4  17776  mvrfval  18644  mplcoe1  18689  mplcoe5  18692  evlsval  18742  ply1coe  18889  ply1coeOLD  18890  coe1fzgsumd  18896  evls1fval  18908  evl1gsumd  18945  gsumfsum  19034  mavmul0  19577  m2detleiblem3  19654  m2detleiblem4  19655  madugsum  19668  cramer0  19715  pmatcollpw3fi1lem1  19810  restco  20180  cnmpt1t  20680  cnmpt2t  20688  fmval  20958  symgtgp  21116  prdstgpd  21139  dfarea  23886  istrkg2ld  24508  wlknwwlknbij2  25442  wlkiswwlkbij2  25449  wwlkextbij  25461  gsumvsca1  28545  gsumvsca2  28546  indv  28834  gsumesum  28880  esumlub  28881  esum2d  28914  sitg0  29179  sdclem2  32071  mpteq1i  37452  stoweidlem9  37869  sge0sn  38221  sge0iunmptlemfi  38255  sge0isum  38269  ovn02  38390  usgedgleord  39784  usgedgleordALT  39785
  Copyright terms: Public domain W3C validator