Theorem cbvmpt 5207

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 2406. See cbvmptg 5208 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 2927	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2927	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvmpt.1	. 2 ⊢ Ⅎ𝑦𝐵
4		cbvmpt.2	. 2 ⊢ Ⅎ𝑥𝐶
5		cbvmpt.3	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
6	1, 2, 3, 4, 5	cbvmptf 5205	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1563  Ⅎwnfc 2912   ↦ cmpt 5186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5168  df-mpt 5187

This theorem is referenced by:  dffn5f  6942  fvmpts  6983  fvmpt2i  6990  fvmptex  6994  fmptcof  7116  fmptcos  7117  fliftfuns  7302  offval2  7684  ofmpteq  7687  mpocurryvald  8254  qliftfuns  8790  axcc2  10409  seqof2  14087  summolem2a  15756  zsum  15759  fsumcvg2  15768  fsumrlim  15853  cbvprod  15957  prodmolem2a  15978  zprod  15981  fprod  15985  pcmptdvds  16944  prdsdsval2  17527  gsumconstf  19996  gsummpt1n0  20026  gsum2d2  20035  dprd2d2  20107  gsumdixp  20391  psrass1lem  22043  coe1fzgsumdlem  22424  gsumply1eq  22430  evl1gsumdlem  22477  madugsum  22761  cnmpt1t  23783  cnmpt2k  23806  elmptrab  23945  flfcnp2  24125  prdsxmet  24487  fsumcn  24990  ovoliunlem3  25624  ovoliun  25625  ovoliun2  25626  voliun  25674  mbfpos  25771  mbfposb  25773  i1fposd  25827  itg2cnlem1  25881  isibl2  25886  cbvitg  25896  itgss3  25935  itgfsum  25947  itgabs  25955  itgcn  25965  limcmpt  26003  dvmptfsum  26095  lhop2  26135  dvfsumle  26141  dvfsumlem2  26147  itgsubstlem  26168  itgsubst  26169  itgulm2  26530  rlimcnp2  27089  gsummpt2co  33281  gsumpart  33296  esumsnf  34371  mbfposadd  38178  itgabsnc  38200  ftc1cnnclem  38202  ftc2nc  38213  zndvdchrrhm  42602  aks6d1c1  42745  evl1gprodd  42746  aks6d1c2  42759  idomnnzgmulnz  42762  deg1gprod  42769  sticksstones12a  42786  aks6d1c6lem5  42806  aks6d1c7lem2  42810  aks6d1c7lem3  42811  aks5lem4a  42819  mzpsubst  43341  rabdiophlem2  43391  aomclem8  43650  fsumcnf  45599  disjf1  45759  disjrnmpt2  45764  disjinfi  45768  fmptf  45812  cncfmptss  46161  mulc1cncfg  46163  expcnfg  46165  fprodcn  46174  fnlimabslt  46251  climmptf  46253  liminfvalxr  46355  liminfpnfuz  46388  xlimpnfxnegmnf2  46430  icccncfext  46459  cncficcgt0  46460  cncfiooicclem1  46465  fprodcncf  46472  dvmptmulf  46509  iblsplitf  46542  stoweidlem21  46593  stirlinglem4  46649  stirlinglem13  46658  stirlinglem15  46660  fourierd  46794  fourierclimd  46795  sge0iunmptlemre  46987  sge0iunmpt  46990  sge0ltfirpmpt2  46998  sge0isummpt2  47004  sge0xaddlem2  47006  sge0xadd  47007  meadjiun  47038  meaiunincf  47055  meaiuninc3  47057  omeiunle  47089  caratheodorylem2  47099  ovncvrrp  47136  vonioo  47254  smflim2  47378  smfsup  47386  smfinf  47390  smflimsup  47400  smfliminf  47403