Theorem mpteq1d 5200

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

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-mpt 5192

This theorem is referenced by:  csbmpt2  5521  mptimass  6047  fmptapd  7148  offval  7665  mposn  8085  offsplitfpar  8101  mpocurryd  8251  cantnff  9634  dfac12lem1  10104  ackbij2lem2  10199  swrd00  14616  swrdlend  14625  swrd0  14630  repswswrd  14756  repswrevw  14759  revco  14807  ccatco  14808  ofccat  14942  vdwapfval  16949  imasdsval  17485  mrcfval  17576  catidd  17648  curfpropd  18201  pwspjmhm  18764  grpinvfval  18917  grpinvfvalALT  18918  psgnfval  19437  psgnfvalfi  19450  odfval  19469  odfvalALT  19470  frgpup3lem  19714  gsum2d2  19911  gsumxp  19913  telgsumfzs  19926  dprd2d2  19983  srgbinom  20147  gsummgp0  20234  pwsco1rhm  20418  pwsco2rhm  20419  funcrngcsetc  20556  funcrngcsetcALT  20557  funcringcsetc  20590  staffval  20757  freshmansdream  21491  phlpropd  21571  pjfval  21622  asclfval  21795  asclpropd  21813  mpfrcl  21999  evlsval  22000  psdffval  22051  evls1rhmlem  22215  evl1fval  22222  mvmulfval  22436  submafval  22473  mdetfval  22480  nfimdetndef  22483  mdetfval1  22484  mdet0pr  22486  m1detdiag  22491  madufval  22531  minmar1fval  22540  gsummatr01  22553  pmatcollpw3fi1lem2  22681  pmatcollpw3fi1  22682  cpmadugsumlemF  22770  ispnrm  23233  ptval2  23495  ptpjcn  23505  xkoptsub  23548  kqval  23620  pt1hmeo  23700  fmval  23837  tmdgsum  23989  subgtgp  23999  prdstmdd  24018  prdsxmslem2  24424  nmfval  24483  lebnumlem1  24867  limcmpt2  25792  dvcmulf  25855  mdegfval  25974  ulmshft  26306  wwlksnextbij  29839  off2  32572  of0r  32609  mptiffisupp  32623  mptprop  32628  fmptunsnop  32630  gsummpt2co  32995  gsumhashmul  33008  gsumwrd2dccat  33014  elrgspnlem4  33203  elrspunidl  33406  evl1deg2  33553  algextdeglem4  33717  esumnul  34045  ofcfval4  34102  measdivcst  34221  omsfval  34292  signstfval  34562  signstf0  34566  signstfvn  34567  mrsubffval  35501  mrsubfval  35502  msubfval  35518  elmsubrn  35522  mvhfval  35527  msrfval  35531  fwddifval  36157  tailfval  36367  curf  37599  poimirlem24  37645  ftc1anc  37702  sdclem2  37743  erngfset  40800  erngfset-rN  40808  dvhfset  41081  dvhset  41082  zndvdchrrhm  41967  aks4d1p1p6  42068  aks6d1c1  42111  aks6d1c5lem3  42132  sticksstones11  42151  fsuppssindlem2  42587  fsuppssind  42588  mzpclval  42720  mzpcompact2  42747  fsovrfovd  44005  supcnvlimsupmpt  45746  cncfshiftioo  45897  cncfiooicc  45899  dvsinax  45918  iblspltprt  45978  itgspltprt  45984  itgiccshift  45985  dirkercncflem2  46109  fourierdlem90  46201  fourierdlem92  46203  sge0val  46371  sge0prle  46406  sge0ss  46417  sge0iunmptlemfi  46418  sge0p1  46419  sge0iunmptlemre  46420  sge0iunmpt  46423  sge0xp  46434  ismeannd  46472  caratheodorylem1  46531  isomenndlem  46535  hoidmv1lelem2  46597  hoidmvlelem2  46601  hspmbllem2  46632  smflimsuplem1  46825  smflimsuplem4  46828  smflimsuplem7  46831  smflimsup  46833  mgpsumunsn  48353  lmod1zr  48486  iinfssclem1  49047  dfswapf2  49254  swapfval  49255  swapf2vala  49263  swapf2f1o  49269  swapf2f1oaALT  49271  prcofpropd  49372  prcof2a  49382  prcof2  49383  lmdfval  49642  cmdfval  49643