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

Theorem mpteq1d 4505
Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
Hypothesis
Ref Expression
mpteq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
mpteq1d  |-  ( ph  ->  ( x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    ph( x)    C( x)

Proof of Theorem mpteq1d
StepHypRef Expression
1 mpteq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 mpteq1 4504 . 2  |-  ( A  =  B  ->  (
x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
31, 2syl 17 1  |-  ( ph  ->  ( x  e.  A  |->  C )  =  ( x  e.  B  |->  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    |-> cmpt 4482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-ral 2776  df-opab 4483  df-mpt 4484
This theorem is referenced by:  csbmpt2  4755  fmptapd  6104  offval  6553  mpt2sn  6899  mpt2curryd  7028  cantnff  8188  dfac12lem1  8581  ackbij2lem2  8678  swrd00  12777  swrd0val  12780  swrdlend  12790  swrd0  12793  repswswrd  12890  repswrevw  12892  revco  12934  ccatco  12935  vdwapfval  14921  imasdsval  15416  imasdsvalOLD  15428  mrcfval  15514  catidd  15586  curfpropd  16118  pwspjmhm  16615  grpinvfval  16704  psgnfval  17141  psgnfvalfi  17154  odfval  17179  odfvalOLD  17182  frgpup3lem  17427  gsum2d2  17606  gsumxp  17608  telgsumfzs  17619  dprd2d2  17677  srgbinom  17778  gsummgp0  17836  pwsco1rhm  17966  pwsco2rhm  17967  staffval  18075  asclfval  18558  asclpropd  18570  mpfrcl  18741  evlsval  18742  evls1rhmlem  18910  evl1fval  18916  phlpropd  19221  pjfval  19268  mvmulfval  19566  submafval  19603  mdetfval  19610  nfimdetndef  19613  mdetfval1  19614  mdet0pr  19616  m1detdiag  19621  madufval  19661  minmar1fval  19670  gsummatr01  19683  pmatcollpw3fi1lem2  19810  pmatcollpw3fi1  19811  cpmadugsumlemF  19899  ispnrm  20354  ptval2  20615  ptpjcn  20625  xkoptsub  20668  kqval  20740  pt1hmeo  20820  fmval  20957  tmdgsum  21109  subgtgp  21119  prdstmdd  21137  prdsxmslem2  21543  nmfval  21602  lebnumlem1  21988  lebnumlem1OLD  21991  limcmpt2  22838  dvcmulf  22898  mdegfval  23010  ulmshft  23344  wwlkextbij  25460  off2  28245  gsummpt2co  28551  esumnul  28878  ofcfval4  28935  measdivcst  29056  omsfval  29127  omsfvalOLD  29131  ofccat  29438  signstfval  29462  signstf0  29466  signstfvn  29467  mrsubffval  30154  mrsubfval  30155  msubfval  30171  elmsubrn  30175  mvhfval  30180  msrfval  30184  fwddifval  30935  tailfval  31034  poimirlem24  31929  ftc1anc  31990  sdclem2  32036  erngfset  34336  erngfset-rN  34344  dvhfset  34618  dvhset  34619  mzpclval  35537  mzpcompact2  35564  cncfshiftioo  37711  cncfiooicc  37713  dvsinax  37724  iblspltprt  37791  itgspltprt  37797  itgiccshift  37798  dirkercncflem2  37907  fourierdlem90  38001  fourierdlem92  38003  sge0val  38117  sge0prle  38152  sge0ss  38163  sge0iunmptlemfi  38164  sge0p1  38165  sge0iunmptlemre  38166  sge0iunmpt  38169  sge0xp  38180  ismeannd  38214  caratheodorylem1  38256  isomenndlem  38260  hoidmv1lelem2  38319  hoidmvlelem2  38323  funcrngcsetc  39649  funcrngcsetcALT  39650  funcringcsetc  39686  mgpsumunsn  39794  lmod1zr  39937
  Copyright terms: Public domain W3C validator