Theorem mpteq1d 5141

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 5140	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1537   ↦ cmpt 5132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-opab 5115  df-mpt 5133

This theorem is referenced by:  csbmpt2  5431  fmptapd  6919  offval  7402  mposn  7784  offsplitfpar  7801  mpocurryd  7921  cantnff  9123  dfac12lem1  9555  ackbij2lem2  9648  swrd00  13991  swrdlend  14000  swrd0  14005  repswswrd  14131  repswrevw  14134  revco  14181  ccatco  14182  ofccat  14314  vdwapfval  16290  imasdsval  16771  mrcfval  16862  catidd  16934  curfpropd  17466  pwspjmhm  17977  grpinvfval  18125  grpinvfvalALT  18126  psgnfval  18611  psgnfvalfi  18624  odfval  18643  odfvalALT  18644  frgpup3lem  18886  gsum2d2  19077  gsumxp  19079  telgsumfzs  19092  dprd2d2  19149  srgbinom  19278  gsummgp0  19341  pwsco1rhm  19473  pwsco2rhm  19474  staffval  19601  asclfval  20091  asclpropd  20109  mpfrcl  20281  evlsval  20282  evls1rhmlem  20467  evl1fval  20474  phlpropd  20782  pjfval  20833  mvmulfval  21134  submafval  21171  mdetfval  21178  nfimdetndef  21181  mdetfval1  21182  mdet0pr  21184  m1detdiag  21189  madufval  21229  minmar1fval  21238  gsummatr01  21251  pmatcollpw3fi1lem2  21378  pmatcollpw3fi1  21379  cpmadugsumlemF  21467  ispnrm  21930  ptval2  22192  ptpjcn  22202  xkoptsub  22245  kqval  22317  pt1hmeo  22397  fmval  22534  tmdgsum  22686  subgtgp  22696  prdstmdd  22715  prdsxmslem2  23122  nmfval  23181  lebnumlem1  23548  limcmpt2  24467  dvcmulf  24527  mdegfval  24642  ulmshft  24964  wwlksnextbij  27666  off2  30374  mptprop  30420  gsummpt2co  30693  freshmansdream  30866  esumnul  31314  ofcfval4  31371  measdivcst  31490  omsfval  31559  signstfval  31841  signstf0  31845  signstfvn  31846  mrsubffval  32761  mrsubfval  32762  msubfval  32778  elmsubrn  32782  mvhfval  32787  msrfval  32791  fwddifval  33630  tailfval  33727  curf  34904  poimirlem24  34950  ftc1anc  35007  sdclem2  35049  erngfset  37967  erngfset-rN  37975  dvhfset  38248  dvhset  38249  mzpclval  39414  mzpcompact2  39441  fsovrfovd  40445  mptima2  41607  supcnvlimsupmpt  42112  cncfshiftioo  42265  cncfiooicc  42267  dvsinax  42287  iblspltprt  42348  itgspltprt  42354  itgiccshift  42355  dirkercncflem2  42479  fourierdlem90  42571  fourierdlem92  42573  sge0val  42738  sge0prle  42773  sge0ss  42784  sge0iunmptlemfi  42785  sge0p1  42786  sge0iunmptlemre  42787  sge0iunmpt  42790  sge0xp  42801  ismeannd  42839  caratheodorylem1  42898  isomenndlem  42902  hoidmv1lelem2  42964  hoidmvlelem2  42968  hspmbllem2  42999  smflimsuplem1  43184  smflimsuplem4  43187  smflimsuplem7  43190  smflimsup  43192  funcrngcsetc  44354  funcrngcsetcALT  44355  funcringcsetc  44391  mgpsumunsn  44494  lmod1zr  44633