Theorem cbvmpt 5223

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

Syntax hints:   → wi 4   = wceq 1540  Ⅎwnfc 2883   ↦ cmpt 5201

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-opab 5182  df-mpt 5202

This theorem is referenced by:  cbvmptvOLD  5226  dffn5f  6949  fvmpts  6988  fvmpt2i  6995  fvmptex  6999  fmptcof  7119  fmptcos  7120  fliftfuns  7306  offval2  7689  ofmpteq  7692  mpocurryvald  8267  qliftfuns  8816  axcc2  10449  seqof2  14076  summolem2a  15729  zsum  15732  fsumcvg2  15741  fsumrlim  15825  cbvprod  15927  prodmolem2a  15948  zprod  15951  fprod  15955  pcmptdvds  16912  prdsdsval2  17496  gsumconstf  19914  gsummpt1n0  19944  gsum2d2  19953  dprd2d2  20025  gsumdixp  20277  psrass1lem  21890  coe1fzgsumdlem  22239  gsumply1eq  22245  evl1gsumdlem  22292  madugsum  22579  cnmpt1t  23601  cnmpt2k  23624  elmptrab  23763  flfcnp2  23943  prdsxmet  24306  fsumcn  24810  ovoliunlem3  25455  ovoliun  25456  ovoliun2  25457  voliun  25505  mbfpos  25602  mbfposb  25604  i1fposd  25658  itg2cnlem1  25712  isibl2  25717  cbvitg  25727  itgss3  25766  itgfsum  25778  itgabs  25786  itgcn  25796  limcmpt  25834  dvmptfsum  25929  lhop2  25970  dvfsumle  25976  dvfsumleOLD  25977  dvfsumlem2  25983  dvfsumlem2OLD  25984  itgsubstlem  26005  itgsubst  26006  itgulm2  26368  rlimcnp2  26926  gsummpt2co  32988  gsumpart  32997  esumsnf  34041  mbfposadd  37637  itgabsnc  37659  ftc1cnnclem  37661  ftc2nc  37672  zndvdchrrhm  41931  aks6d1c1  42075  evl1gprodd  42076  aks6d1c2  42089  idomnnzgmulnz  42092  deg1gprod  42099  sticksstones12a  42116  aks6d1c6lem5  42136  aks6d1c7lem2  42140  aks6d1c7lem3  42141  aks5lem4a  42149  mzpsubst  42718  rabdiophlem2  42772  aomclem8  43032  fsumcnf  44993  disjf1  45155  disjrnmpt2  45160  disjinfi  45164  fmptf  45211  cncfmptss  45564  mulc1cncfg  45566  expcnfg  45568  fprodcn  45577  fnlimabslt  45656  climmptf  45658  liminfvalxr  45760  liminfpnfuz  45793  xlimpnfxnegmnf2  45835  icccncfext  45864  cncficcgt0  45865  cncfiooicclem1  45870  fprodcncf  45877  dvmptmulf  45914  iblsplitf  45947  stoweidlem21  45998  stirlinglem4  46054  stirlinglem13  46063  stirlinglem15  46065  fourierd  46199  fourierclimd  46200  sge0iunmptlemre  46392  sge0iunmpt  46395  sge0ltfirpmpt2  46403  sge0isummpt2  46409  sge0xaddlem2  46411  sge0xadd  46412  meadjiun  46443  meaiunincf  46460  meaiuninc3  46462  omeiunle  46494  caratheodorylem2  46504  ovncvrrp  46541  vonioo  46659  smflim2  46783  smfsup  46791  smfinf  46795  smflimsup  46805  smfliminf  46808