Theorem cbvmpt 5187

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 5188 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 5185	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1542  Ⅎwnfc 2883   ↦ cmpt 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5148  df-mpt 5167

This theorem is referenced by:  dffn5f  6911  fvmpts  6951  fvmpt2i  6958  fvmptex  6962  fmptcof  7083  fmptcos  7084  fliftfuns  7269  offval2  7651  ofmpteq  7654  mpocurryvald  8220  qliftfuns  8751  axcc2  10359  seqof2  14022  summolem2a  15677  zsum  15680  fsumcvg2  15689  fsumrlim  15774  cbvprod  15878  prodmolem2a  15899  zprod  15902  fprod  15906  pcmptdvds  16865  prdsdsval2  17447  gsumconstf  19910  gsummpt1n0  19940  gsum2d2  19949  dprd2d2  20021  gsumdixp  20298  psrass1lem  21912  coe1fzgsumdlem  22268  gsumply1eq  22274  evl1gsumdlem  22321  madugsum  22608  cnmpt1t  23630  cnmpt2k  23653  elmptrab  23792  flfcnp2  23972  prdsxmet  24334  fsumcn  24837  ovoliunlem3  25471  ovoliun  25472  ovoliun2  25473  voliun  25521  mbfpos  25618  mbfposb  25620  i1fposd  25674  itg2cnlem1  25728  isibl2  25733  cbvitg  25743  itgss3  25782  itgfsum  25794  itgabs  25802  itgcn  25812  limcmpt  25850  dvmptfsum  25942  lhop2  25982  dvfsumle  25988  dvfsumlem2  25994  itgsubstlem  26015  itgsubst  26016  itgulm2  26374  rlimcnp2  26930  gsummpt2co  33109  gsumpart  33124  esumsnf  34208  mbfposadd  37988  itgabsnc  38010  ftc1cnnclem  38012  ftc2nc  38023  zndvdchrrhm  42412  aks6d1c1  42555  evl1gprodd  42556  aks6d1c2  42569  idomnnzgmulnz  42572  deg1gprod  42579  sticksstones12a  42596  aks6d1c6lem5  42616  aks6d1c7lem2  42620  aks6d1c7lem3  42621  aks5lem4a  42629  mzpsubst  43180  rabdiophlem2  43230  aomclem8  43489  fsumcnf  45452  disjf1  45613  disjrnmpt2  45618  disjinfi  45622  fmptf  45668  cncfmptss  46017  mulc1cncfg  46019  expcnfg  46021  fprodcn  46030  fnlimabslt  46107  climmptf  46109  liminfvalxr  46211  liminfpnfuz  46244  xlimpnfxnegmnf2  46286  icccncfext  46315  cncficcgt0  46316  cncfiooicclem1  46321  fprodcncf  46328  dvmptmulf  46365  iblsplitf  46398  stoweidlem21  46449  stirlinglem4  46505  stirlinglem13  46514  stirlinglem15  46516  fourierd  46650  fourierclimd  46651  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0ltfirpmpt2  46854  sge0isummpt2  46860  sge0xaddlem2  46862  sge0xadd  46863  meadjiun  46894  meaiunincf  46911  meaiuninc3  46913  omeiunle  46945  caratheodorylem2  46955  ovncvrrp  46992  vonioo  47110  smflim2  47234  smfsup  47242  smfinf  47246  smflimsup  47256  smfliminf  47259