Theorem cbvmpt 5197

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.) Add disjoint variable condition to avoid ax-13 2370. See cbvmptg 5198 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.)

Hypotheses

Ref	Expression
cbvmpt.1	⊢ Ⅎ𝑦𝐵
cbvmpt.2	⊢ Ⅎ𝑥𝐶
cbvmpt.3	⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)

Assertion

Ref	Expression
cbvmpt	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Distinct variable group:   𝑥,𝑦,𝐴

Allowed substitution hints:   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Proof of Theorem cbvmpt

Step	Hyp	Ref	Expression
1		nfcv 2891	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2891	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvmpt.1	. 2 ⊢ Ⅎ𝑦𝐵
4		cbvmpt.2	. 2 ⊢ Ⅎ𝑥𝐶
5		cbvmpt.3	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
6	1, 2, 3, 4, 5	cbvmptf 5195	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1540  Ⅎwnfc 2876   ↦ cmpt 5176

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-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-opab 5158  df-mpt 5177

This theorem is referenced by:  dffn5f  6898  fvmpts  6937  fvmpt2i  6944  fvmptex  6948  fmptcof  7068  fmptcos  7069  fliftfuns  7255  offval2  7637  ofmpteq  7640  mpocurryvald  8210  qliftfuns  8738  axcc2  10350  seqof2  13985  summolem2a  15640  zsum  15643  fsumcvg2  15652  fsumrlim  15736  cbvprod  15838  prodmolem2a  15859  zprod  15862  fprod  15866  pcmptdvds  16824  prdsdsval2  17406  gsumconstf  19832  gsummpt1n0  19862  gsum2d2  19871  dprd2d2  19943  gsumdixp  20222  psrass1lem  21857  coe1fzgsumdlem  22206  gsumply1eq  22212  evl1gsumdlem  22259  madugsum  22546  cnmpt1t  23568  cnmpt2k  23591  elmptrab  23730  flfcnp2  23910  prdsxmet  24273  fsumcn  24777  ovoliunlem3  25421  ovoliun  25422  ovoliun2  25423  voliun  25471  mbfpos  25568  mbfposb  25570  i1fposd  25624  itg2cnlem1  25678  isibl2  25683  cbvitg  25693  itgss3  25732  itgfsum  25744  itgabs  25752  itgcn  25762  limcmpt  25800  dvmptfsum  25895  lhop2  25936  dvfsumle  25942  dvfsumleOLD  25943  dvfsumlem2  25949  dvfsumlem2OLD  25950  itgsubstlem  25971  itgsubst  25972  itgulm2  26334  rlimcnp2  26892  gsummpt2co  33014  gsumpart  33023  esumsnf  34030  mbfposadd  37646  itgabsnc  37668  ftc1cnnclem  37670  ftc2nc  37681  zndvdchrrhm  41945  aks6d1c1  42089  evl1gprodd  42090  aks6d1c2  42103  idomnnzgmulnz  42106  deg1gprod  42113  sticksstones12a  42130  aks6d1c6lem5  42150  aks6d1c7lem2  42154  aks6d1c7lem3  42155  aks5lem4a  42163  mzpsubst  42721  rabdiophlem2  42775  aomclem8  43034  fsumcnf  44999  disjf1  45161  disjrnmpt2  45166  disjinfi  45170  fmptf  45217  cncfmptss  45569  mulc1cncfg  45571  expcnfg  45573  fprodcn  45582  fnlimabslt  45661  climmptf  45663  liminfvalxr  45765  liminfpnfuz  45798  xlimpnfxnegmnf2  45840  icccncfext  45869  cncficcgt0  45870  cncfiooicclem1  45875  fprodcncf  45882  dvmptmulf  45919  iblsplitf  45952  stoweidlem21  46003  stirlinglem4  46059  stirlinglem13  46068  stirlinglem15  46070  fourierd  46204  fourierclimd  46205  sge0iunmptlemre  46397  sge0iunmpt  46400  sge0ltfirpmpt2  46408  sge0isummpt2  46414  sge0xaddlem2  46416  sge0xadd  46417  meadjiun  46448  meaiunincf  46465  meaiuninc3  46467  omeiunle  46499  caratheodorylem2  46509  ovncvrrp  46546  vonioo  46664  smflim2  46788  smfsup  46796  smfinf  46800  smflimsup  46810  smfliminf  46813