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 2372. See cbvmptg 5182 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 2906	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2906	. 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 1539  Ⅎwnfc 2886   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-mpt 5154

This theorem is referenced by:  cbvmptvOLD  5184  dffn5f  6822  fvmpts  6860  fvmpt2i  6867  fvmptex  6871  fmptcof  6984  fmptcos  6985  fliftfuns  7165  offval2  7531  ofmpteq  7533  mpocurryvald  8057  qliftfuns  8551  axcc2  10124  seqof2  13709  summolem2a  15355  zsum  15358  fsumcvg2  15367  fsumrlim  15451  cbvprod  15553  prodmolem2a  15572  zprod  15575  fprod  15579  pcmptdvds  16523  prdsdsval2  17112  gsumconstf  19451  gsummpt1n0  19481  gsum2d2  19490  dprd2d2  19562  gsumdixp  19763  psrass1lemOLD  21053  psrass1lem  21056  coe1fzgsumdlem  21382  gsumply1eq  21386  evl1gsumdlem  21432  madugsum  21700  cnmpt1t  22724  cnmpt2k  22747  elmptrab  22886  flfcnp2  23066  prdsxmet  23430  fsumcn  23939  ovoliunlem3  24573  ovoliun  24574  ovoliun2  24575  voliun  24623  mbfpos  24720  mbfposb  24722  i1fposd  24777  itg2cnlem1  24831  isibl2  24836  cbvitg  24845  itgss3  24884  itgfsum  24896  itgabs  24904  itgcn  24914  limcmpt  24952  dvmptfsum  25044  lhop2  25084  dvfsumle  25090  dvfsumlem2  25096  itgsubstlem  25117  itgsubst  25118  itgulm2  25473  rlimcnp2  26021  gsummpt2co  31210  gsumpart  31217  esumsnf  31932  mbfposadd  35751  itgabsnc  35773  ftc1cnnclem  35775  ftc2nc  35786  sticksstones12a  40041  mzpsubst  40486  rabdiophlem2  40540  aomclem8  40802  fsumcnf  42453  disjf1  42609  disjrnmpt2  42615  disjinfi  42620  fmptf  42672  cncfmptss  43018  mulc1cncfg  43020  expcnfg  43022  fprodcn  43031  fnlimabslt  43110  climmptf  43112  liminfvalxr  43214  liminfpnfuz  43247  xlimpnfxnegmnf2  43289  icccncfext  43318  cncficcgt0  43319  cncfiooicclem1  43324  fprodcncf  43331  dvmptmulf  43368  iblsplitf  43401  stoweidlem21  43452  stirlinglem4  43508  stirlinglem13  43517  stirlinglem15  43519  fourierd  43653  fourierclimd  43654  sge0iunmptlemre  43843  sge0iunmpt  43846  sge0ltfirpmpt2  43854  sge0isummpt2  43860  sge0xaddlem2  43862  sge0xadd  43863  meadjiun  43894  meaiunincf  43911  meaiuninc3  43913  omeiunle  43945  caratheodorylem2  43955  ovncvrrp  43992  vonioo  44110  smflim2  44226  smfsup  44234  smfinf  44238  smflimsup  44248  smfliminf  44251