Theorem cbvmpt 5211

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Ⅎwnfc 2909   ↦ cmpt 5190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5172  df-mpt 5191

This theorem is used by:  dffn5f  6953  fvmpts  6994  fvmpt2i  7001  fvmptex  7005  fmptcof  7127  fmptcos  7128  fliftfuns  7318  offval2  7701  ofmpteq  7704  mpocurryvald  8271  qliftfuns  8807  axcc2  10442  seqof2  14126  summolem2a  15803  zsum  15806  fsumcvg2  15815  fsumrlim  15900  cbvprod  16004  prodmolem2a  16025  zprod  16028  fprod  16032  pcmptdvds  16990  prdsdsval2  17573  gsumconstf  20066  gsummpt1n0  20096  gsum2d2  20105  dprd2d2  20177  gsumdixp  20463  psrass1lem  22152  coe1fzgsumdlem  22532  gsumply1eq  22538  evl1gsumdlem  22585  madugsum  22869  cnmpt1t  23895  cnmpt2k  23918  elmptrab  24057  flfcnp2  24237  prdsxmet  24599  fsumcn  25102  ovoliunlem3  25736  ovoliun  25737  ovoliun2  25738  voliun  25786  mbfpos  25883  mbfposb  25885  i1fposd  25939  itg2cnlem1  25993  isibl2  25998  cbvitg  26008  itgss3  26047  itgfsum  26059  itgabs  26067  itgcn  26077  limcmpt  26115  dvmptfsum  26207  lhop2  26247  dvfsumle  26253  dvfsumlem2  26259  itgsubstlem  26280  itgsubst  26281  itgulm2  26645  rlimcnp2  27204  gsummpt2co  33490  gsumpart  33505  esumsnf  34576  mbfposadd  38418  itgabsnc  38440  ftc1cnnclem  38442  ftc2nc  38453  zndvdchrrhm  42841  aks6d1c1  42984  evl1gprodd  42985  aks6d1c2  42998  idomnnzgmulnz  43001  deg1gprod  43008  sticksstones12a  43025  aks6d1c6lem5  43045  aks6d1c7lem2  43049  aks6d1c7lem3  43050  aks5lem4a  43058  mzpsubst  43595  rabdiophlem2  43645  aomclem8  43904  fsumcnf  45857  disjf1  46017  disjrnmpt2  46022  disjinfi  46026  fmptf  46070  cncfmptss  46419  mulc1cncfg  46421  expcnfg  46423  fprodcn  46432  fnlimabslt  46509  climmptf  46511  liminfvalxr  46613  liminfpnfuz  46646  xlimpnfxnegmnf2  46688  icccncfext  46717  cncficcgt0  46718  cncfiooicclem1  46723  fprodcncf  46730  dvmptmulf  46767  iblsplitf  46800  stoweidlem21  46851  stirlinglem4  46907  stirlinglem13  46916  stirlinglem15  46918  fourierd  47052  fourierclimd  47053  sge0iunmptlemre  47245  sge0iunmpt  47248  sge0ltfirpmpt2  47256  sge0isummpt2  47262  sge0xaddlem2  47264  sge0xadd  47265  meadjiun  47296  meaiunincf  47313  meaiuninc3  47315  omeiunle  47347  caratheodorylem2  47357  ovncvrrp  47394  vonioo  47512  smflim2  47636  smfsup  47644  smfinf  47648  smflimsup  47658  smfliminf  47661