Theorem cbvmpt 5212

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-opab 5173  df-mpt 5192

This theorem is used by:  dffn5f  6952  fvmpts  6993  fvmpt2i  7000  fvmptex  7004  fmptcof  7126  fmptcos  7127  fliftfuns  7312  offval2  7696  ofmpteq  7699  mpocurryvald  8264  qliftfuns  8800  axcc2  10427  seqof2  14103  summolem2a  15773  zsum  15776  fsumcvg2  15785  fsumrlim  15870  cbvprod  15974  prodmolem2a  15995  zprod  15998  fprod  16002  pcmptdvds  16960  prdsdsval2  17543  gsumconstf  20011  gsummpt1n0  20041  gsum2d2  20050  dprd2d2  20122  gsumdixp  20407  psrass1lem  22094  coe1fzgsumdlem  22474  gsumply1eq  22480  evl1gsumdlem  22527  madugsum  22811  cnmpt1t  23833  cnmpt2k  23856  elmptrab  23995  flfcnp2  24175  prdsxmet  24537  fsumcn  25040  ovoliunlem3  25674  ovoliun  25675  ovoliun2  25676  voliun  25724  mbfpos  25821  mbfposb  25823  i1fposd  25877  itg2cnlem1  25931  isibl2  25936  cbvitg  25946  itgss3  25985  itgfsum  25997  itgabs  26005  itgcn  26015  limcmpt  26053  dvmptfsum  26145  lhop2  26185  dvfsumle  26191  dvfsumlem2  26197  itgsubstlem  26218  itgsubst  26219  itgulm2  26583  rlimcnp2  27142  gsummpt2co  33377  gsumpart  33392  esumsnf  34463  mbfposadd  38346  itgabsnc  38368  ftc1cnnclem  38370  ftc2nc  38381  zndvdchrrhm  42768  aks6d1c1  42911  evl1gprodd  42912  aks6d1c2  42925  idomnnzgmulnz  42928  deg1gprod  42935  sticksstones12a  42952  aks6d1c6lem5  42972  aks6d1c7lem2  42976  aks6d1c7lem3  42977  aks5lem4a  42985  mzpsubst  43507  rabdiophlem2  43557  aomclem8  43816  fsumcnf  45769  disjf1  45929  disjrnmpt2  45934  disjinfi  45938  fmptf  45982  cncfmptss  46331  mulc1cncfg  46333  expcnfg  46335  fprodcn  46344  fnlimabslt  46421  climmptf  46423  liminfvalxr  46525  liminfpnfuz  46558  xlimpnfxnegmnf2  46600  icccncfext  46629  cncficcgt0  46630  cncfiooicclem1  46635  fprodcncf  46642  dvmptmulf  46679  iblsplitf  46712  stoweidlem21  46763  stirlinglem4  46819  stirlinglem13  46828  stirlinglem15  46830  fourierd  46964  fourierclimd  46965  sge0iunmptlemre  47157  sge0iunmpt  47160  sge0ltfirpmpt2  47168  sge0isummpt2  47174  sge0xaddlem2  47176  sge0xadd  47177  meadjiun  47208  meaiunincf  47225  meaiuninc3  47227  omeiunle  47259  caratheodorylem2  47269  ovncvrrp  47306  vonioo  47424  smflim2  47548  smfsup  47556  smfinf  47560  smflimsup  47570  smfliminf  47573