Theorem cbvmpt 5181

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

Syntax hints:   → wi 4   = wceq 1547  Ⅎwnfc 2887   ↦ cmpt 5160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5142  df-mpt 5161

This theorem is referenced by:  dffn5f  6905  fvmpts  6946  fvmpt2i  6953  fvmptex  6957  fmptcof  7079  fmptcos  7080  fliftfuns  7265  offval2  7647  ofmpteq  7650  mpocurryvald  8217  qliftfuns  8748  axcc2  10357  seqof2  14020  summolem2a  15675  zsum  15678  fsumcvg2  15687  fsumrlim  15772  cbvprod  15876  prodmolem2a  15897  zprod  15900  fprod  15904  pcmptdvds  16863  prdsdsval2  17445  gsumconstf  19908  gsummpt1n0  19938  gsum2d2  19947  dprd2d2  20019  gsumdixp  20296  psrass1lem  21915  coe1fzgsumdlem  22296  gsumply1eq  22302  evl1gsumdlem  22349  madugsum  22633  cnmpt1t  23655  cnmpt2k  23678  elmptrab  23817  flfcnp2  23997  prdsxmet  24359  fsumcn  24862  ovoliunlem3  25496  ovoliun  25497  ovoliun2  25498  voliun  25546  mbfpos  25643  mbfposb  25645  i1fposd  25699  itg2cnlem1  25753  isibl2  25758  cbvitg  25768  itgss3  25807  itgfsum  25819  itgabs  25827  itgcn  25837  limcmpt  25875  dvmptfsum  25967  lhop2  26007  dvfsumle  26013  dvfsumlem2  26019  itgsubstlem  26040  itgsubst  26041  itgulm2  26399  rlimcnp2  26955  gsummpt2co  33136  gsumpart  33151  esumsnf  34255  mbfposadd  38035  itgabsnc  38057  ftc1cnnclem  38059  ftc2nc  38070  zndvdchrrhm  42459  aks6d1c1  42602  evl1gprodd  42603  aks6d1c2  42616  idomnnzgmulnz  42619  deg1gprod  42626  sticksstones12a  42643  aks6d1c6lem5  42663  aks6d1c7lem2  42667  aks6d1c7lem3  42668  aks5lem4a  42676  mzpsubst  43198  rabdiophlem2  43248  aomclem8  43507  fsumcnf  45470  disjf1  45631  disjrnmpt2  45636  disjinfi  45640  fmptf  45684  cncfmptss  46033  mulc1cncfg  46035  expcnfg  46037  fprodcn  46046  fnlimabslt  46123  climmptf  46125  liminfvalxr  46227  liminfpnfuz  46260  xlimpnfxnegmnf2  46302  icccncfext  46331  cncficcgt0  46332  cncfiooicclem1  46337  fprodcncf  46344  dvmptmulf  46381  iblsplitf  46414  stoweidlem21  46465  stirlinglem4  46521  stirlinglem13  46530  stirlinglem15  46532  fourierd  46666  fourierclimd  46667  sge0iunmptlemre  46859  sge0iunmpt  46862  sge0ltfirpmpt2  46870  sge0isummpt2  46876  sge0xaddlem2  46878  sge0xadd  46879  meadjiun  46910  meaiunincf  46927  meaiuninc3  46929  omeiunle  46961  caratheodorylem2  46971  ovncvrrp  47008  vonioo  47126  smflim2  47250  smfsup  47258  smfinf  47262  smflimsup  47272  smfliminf  47275