Theorem cbvmpt 5141

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

Syntax hints:   → wi 4   = wceq 1542  Ⅎwnfc 2880   ↦ cmpt 5120

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-v 3402  df-un 3858  df-sn 4527  df-pr 4529  df-op 4533  df-opab 5103  df-mpt 5121

This theorem is referenced by:  cbvmptv  5143  dffn5f  6753  fvmpts  6791  fvmpt2i  6798  fvmptex  6802  fmptcof  6915  fmptcos  6916  fliftfuns  7093  offval2  7457  ofmpteq  7459  mpocurryvald  7978  qliftfuns  8428  axcc2  9950  seqof2  13533  summolem2a  15178  zsum  15181  fsumcvg2  15190  fsumrlim  15272  cbvprod  15374  prodmolem2a  15393  zprod  15396  fprod  15400  pcmptdvds  16343  prdsdsval2  16873  gsumconstf  19187  gsummpt1n0  19217  gsum2d2  19226  dprd2d2  19298  gsumdixp  19494  psrass1lemOLD  20766  psrass1lem  20769  coe1fzgsumdlem  21089  gsumply1eq  21093  evl1gsumdlem  21139  madugsum  21407  cnmpt1t  22429  cnmpt2k  22452  elmptrab  22591  flfcnp2  22771  prdsxmet  23135  fsumcn  23635  ovoliunlem3  24269  ovoliun  24270  ovoliun2  24271  voliun  24319  mbfpos  24416  mbfposb  24418  i1fposd  24473  itg2cnlem1  24527  isibl2  24532  cbvitg  24541  itgss3  24580  itgfsum  24592  itgabs  24600  itgcn  24610  limcmpt  24648  dvmptfsum  24740  lhop2  24780  dvfsumle  24786  dvfsumlem2  24792  itgsubstlem  24813  itgsubst  24814  itgulm2  25169  rlimcnp2  25717  gsummpt2co  30898  gsumpart  30905  esumsnf  31615  mbfposadd  35480  itgabsnc  35502  ftc1cnnclem  35504  ftc2nc  35515  sticksstones12a  39752  mzpsubst  40183  rabdiophlem2  40237  aomclem8  40499  fsumcnf  42143  disjf1  42299  disjrnmpt2  42305  disjinfi  42310  fmptf  42361  cncfmptss  42711  mulc1cncfg  42713  expcnfg  42715  fprodcn  42724  fnlimabslt  42803  climmptf  42805  liminfvalxr  42907  liminfpnfuz  42940  xlimpnfxnegmnf2  42982  icccncfext  43011  cncficcgt0  43012  cncfiooicclem1  43017  fprodcncf  43024  dvmptmulf  43061  iblsplitf  43094  stoweidlem21  43145  stirlinglem4  43201  stirlinglem13  43210  stirlinglem15  43212  fourierd  43346  fourierclimd  43347  sge0iunmptlemre  43536  sge0iunmpt  43539  sge0ltfirpmpt2  43547  sge0isummpt2  43553  sge0xaddlem2  43555  sge0xadd  43556  meadjiun  43587  meaiunincf  43604  meaiuninc3  43606  omeiunle  43638  caratheodorylem2  43648  ovncvrrp  43685  vonioo  43803  smflim2  43919  smfsup  43927  smfinf  43931  smflimsup  43941  smfliminf  43944