Theorem cbvmpt 5260

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 2372. See cbvmptg 5261 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 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 2904	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2904	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvmpt.1	. 2 ⊢ Ⅎ𝑦𝐵
4		cbvmpt.2	. 2 ⊢ Ⅎ𝑥𝐶
5		cbvmpt.3	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
6	1, 2, 3, 4, 5	cbvmptf 5258	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1542  Ⅎwnfc 2884   ↦ cmpt 5232

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-opab 5212  df-mpt 5233

This theorem is referenced by:  cbvmptvOLD  5263  dffn5f  6964  fvmpts  7002  fvmpt2i  7009  fvmptex  7013  fmptcof  7128  fmptcos  7129  fliftfuns  7311  offval2  7690  ofmpteq  7692  mpocurryvald  8255  qliftfuns  8798  axcc2  10432  seqof2  14026  summolem2a  15661  zsum  15664  fsumcvg2  15673  fsumrlim  15757  cbvprod  15859  prodmolem2a  15878  zprod  15881  fprod  15885  pcmptdvds  16827  prdsdsval2  17430  gsumconstf  19803  gsummpt1n0  19833  gsum2d2  19842  dprd2d2  19914  gsumdixp  20131  psrass1lemOLD  21493  psrass1lem  21496  coe1fzgsumdlem  21825  gsumply1eq  21829  evl1gsumdlem  21875  madugsum  22145  cnmpt1t  23169  cnmpt2k  23192  elmptrab  23331  flfcnp2  23511  prdsxmet  23875  fsumcn  24386  ovoliunlem3  25021  ovoliun  25022  ovoliun2  25023  voliun  25071  mbfpos  25168  mbfposb  25170  i1fposd  25225  itg2cnlem1  25279  isibl2  25284  cbvitg  25293  itgss3  25332  itgfsum  25344  itgabs  25352  itgcn  25362  limcmpt  25400  dvmptfsum  25492  lhop2  25532  dvfsumle  25538  dvfsumlem2  25544  itgsubstlem  25565  itgsubst  25566  itgulm2  25921  rlimcnp2  26471  gsummpt2co  32200  gsumpart  32207  esumsnf  33062  gg-dvfsumle  35182  gg-dvfsumlem2  35183  mbfposadd  36535  itgabsnc  36557  ftc1cnnclem  36559  ftc2nc  36570  sticksstones12a  40973  mzpsubst  41486  rabdiophlem2  41540  aomclem8  41803  fsumcnf  43705  disjf1  43880  disjrnmpt2  43886  disjinfi  43891  fmptf  43942  cncfmptss  44303  mulc1cncfg  44305  expcnfg  44307  fprodcn  44316  fnlimabslt  44395  climmptf  44397  liminfvalxr  44499  liminfpnfuz  44532  xlimpnfxnegmnf2  44574  icccncfext  44603  cncficcgt0  44604  cncfiooicclem1  44609  fprodcncf  44616  dvmptmulf  44653  iblsplitf  44686  stoweidlem21  44737  stirlinglem4  44793  stirlinglem13  44802  stirlinglem15  44804  fourierd  44938  fourierclimd  44939  sge0iunmptlemre  45131  sge0iunmpt  45134  sge0ltfirpmpt2  45142  sge0isummpt2  45148  sge0xaddlem2  45150  sge0xadd  45151  meadjiun  45182  meaiunincf  45199  meaiuninc3  45201  omeiunle  45233  caratheodorylem2  45243  ovncvrrp  45280  vonioo  45398  smflim2  45522  smfsup  45530  smfinf  45534  smflimsup  45544  smfliminf  45547