Theorem cbvmpt 5253

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

Syntax hints:   → wi 4   = wceq 1540  Ⅎwnfc 2890   ↦ cmpt 5225

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-mpt 5226

This theorem is referenced by:  cbvmptvOLD  5256  dffn5f  6980  fvmpts  7019  fvmpt2i  7026  fvmptex  7030  fmptcof  7150  fmptcos  7151  fliftfuns  7334  offval2  7717  ofmpteq  7720  mpocurryvald  8295  qliftfuns  8844  axcc2  10477  seqof2  14101  summolem2a  15751  zsum  15754  fsumcvg2  15763  fsumrlim  15847  cbvprod  15949  prodmolem2a  15970  zprod  15973  fprod  15977  pcmptdvds  16932  prdsdsval2  17529  gsumconstf  19953  gsummpt1n0  19983  gsum2d2  19992  dprd2d2  20064  gsumdixp  20316  psrass1lem  21952  coe1fzgsumdlem  22307  gsumply1eq  22313  evl1gsumdlem  22360  madugsum  22649  cnmpt1t  23673  cnmpt2k  23696  elmptrab  23835  flfcnp2  24015  prdsxmet  24379  fsumcn  24894  ovoliunlem3  25539  ovoliun  25540  ovoliun2  25541  voliun  25589  mbfpos  25686  mbfposb  25688  i1fposd  25742  itg2cnlem1  25796  isibl2  25801  cbvitg  25811  itgss3  25850  itgfsum  25862  itgabs  25870  itgcn  25880  limcmpt  25918  dvmptfsum  26013  lhop2  26054  dvfsumle  26060  dvfsumleOLD  26061  dvfsumlem2  26067  dvfsumlem2OLD  26068  itgsubstlem  26089  itgsubst  26090  itgulm2  26452  rlimcnp2  27009  gsummpt2co  33051  gsumpart  33060  esumsnf  34065  mbfposadd  37674  itgabsnc  37696  ftc1cnnclem  37698  ftc2nc  37709  zndvdchrrhm  41972  aks6d1c1  42117  evl1gprodd  42118  aks6d1c2  42131  idomnnzgmulnz  42134  deg1gprod  42141  sticksstones12a  42158  aks6d1c6lem5  42178  aks6d1c7lem2  42182  aks6d1c7lem3  42183  aks5lem4a  42191  mzpsubst  42759  rabdiophlem2  42813  aomclem8  43073  fsumcnf  45026  disjf1  45188  disjrnmpt2  45193  disjinfi  45197  fmptf  45245  cncfmptss  45602  mulc1cncfg  45604  expcnfg  45606  fprodcn  45615  fnlimabslt  45694  climmptf  45696  liminfvalxr  45798  liminfpnfuz  45831  xlimpnfxnegmnf2  45873  icccncfext  45902  cncficcgt0  45903  cncfiooicclem1  45908  fprodcncf  45915  dvmptmulf  45952  iblsplitf  45985  stoweidlem21  46036  stirlinglem4  46092  stirlinglem13  46101  stirlinglem15  46103  fourierd  46237  fourierclimd  46238  sge0iunmptlemre  46430  sge0iunmpt  46433  sge0ltfirpmpt2  46441  sge0isummpt2  46447  sge0xaddlem2  46449  sge0xadd  46450  meadjiun  46481  meaiunincf  46498  meaiuninc3  46500  omeiunle  46532  caratheodorylem2  46542  ovncvrrp  46579  vonioo  46697  smflim2  46821  smfsup  46829  smfinf  46833  smflimsup  46843  smfliminf  46846