Theorem mpteq1d 5169

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)

Hypothesis

Ref	Expression
mpteq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
mpteq1d	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq1d

Step	Hyp	Ref	Expression
1		mpteq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		mpteq1 5167	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1539   ↦ cmpt 5157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-mpt 5158

This theorem is referenced by:  csbmpt2  5471  fmptapd  7043  offval  7542  mposn  7943  offsplitfpar  7960  mpocurryd  8085  cantnff  9432  dfac12lem1  9899  ackbij2lem2  9996  swrd00  14357  swrdlend  14366  swrd0  14371  repswswrd  14497  repswrevw  14500  revco  14547  ccatco  14548  ofccat  14680  vdwapfval  16672  imasdsval  17226  mrcfval  17317  catidd  17389  curfpropd  17951  pwspjmhm  18468  grpinvfval  18618  grpinvfvalALT  18619  psgnfval  19108  psgnfvalfi  19121  odfval  19140  odfvalALT  19141  frgpup3lem  19383  gsum2d2  19575  gsumxp  19577  telgsumfzs  19590  dprd2d2  19647  srgbinom  19781  gsummgp0  19847  pwsco1rhm  19982  pwsco2rhm  19983  staffval  20107  phlpropd  20860  pjfval  20913  asclfval  21083  asclpropd  21101  mpfrcl  21295  evlsval  21296  evls1rhmlem  21487  evl1fval  21494  mvmulfval  21691  submafval  21728  mdetfval  21735  nfimdetndef  21738  mdetfval1  21739  mdet0pr  21741  m1detdiag  21746  madufval  21786  minmar1fval  21795  gsummatr01  21808  pmatcollpw3fi1lem2  21936  pmatcollpw3fi1  21937  cpmadugsumlemF  22025  ispnrm  22490  ptval2  22752  ptpjcn  22762  xkoptsub  22805  kqval  22877  pt1hmeo  22957  fmval  23094  tmdgsum  23246  subgtgp  23256  prdstmdd  23275  prdsxmslem2  23685  nmfval  23744  lebnumlem1  24124  limcmpt2  25048  dvcmulf  25109  mdegfval  25227  ulmshft  25549  wwlksnextbij  28267  off2  30978  mptprop  31031  gsummpt2co  31308  gsumhashmul  31316  freshmansdream  31484  elrspunidl  31606  esumnul  32016  ofcfval4  32073  measdivcst  32192  omsfval  32261  signstfval  32543  signstf0  32547  signstfvn  32548  mrsubffval  33469  mrsubfval  33470  msubfval  33486  elmsubrn  33490  mvhfval  33495  msrfval  33499  fwddifval  34464  tailfval  34561  curf  35755  poimirlem24  35801  ftc1anc  35858  sdclem2  35900  erngfset  38813  erngfset-rN  38821  dvhfset  39094  dvhset  39095  aks4d1p1p6  40081  sticksstones11  40112  fsuppssindlem2  40281  fsuppssind  40282  mzpclval  40547  mzpcompact2  40574  fsovrfovd  41617  mptima2  42791  supcnvlimsupmpt  43282  cncfshiftioo  43433  cncfiooicc  43435  dvsinax  43454  iblspltprt  43514  itgspltprt  43520  itgiccshift  43521  dirkercncflem2  43645  fourierdlem90  43737  fourierdlem92  43739  sge0val  43904  sge0prle  43939  sge0ss  43950  sge0iunmptlemfi  43951  sge0p1  43952  sge0iunmptlemre  43953  sge0iunmpt  43956  sge0xp  43967  ismeannd  44005  caratheodorylem1  44064  isomenndlem  44068  hoidmv1lelem2  44130  hoidmvlelem2  44134  hspmbllem2  44165  smflimsuplem1  44353  smflimsuplem4  44356  smflimsuplem7  44359  smflimsup  44361  funcrngcsetc  45556  funcrngcsetcALT  45557  funcringcsetc  45593  mgpsumunsn  45697  lmod1zr  45834