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 2371. 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 2892	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2892	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvmpt.1	. 2 ⊢ Ⅎ𝑦𝐵
4		cbvmpt.2	. 2 ⊢ Ⅎ𝑥𝐶
5		cbvmpt.3	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
6	1, 2, 3, 4, 5	cbvmptf 5210	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1540  Ⅎwnfc 2877   ↦ cmpt 5191

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-opab 5173  df-mpt 5192

This theorem is referenced by:  dffn5f  6935  fvmpts  6974  fvmpt2i  6981  fvmptex  6985  fmptcof  7105  fmptcos  7106  fliftfuns  7292  offval2  7676  ofmpteq  7679  mpocurryvald  8252  qliftfuns  8780  axcc2  10397  seqof2  14032  summolem2a  15688  zsum  15691  fsumcvg2  15700  fsumrlim  15784  cbvprod  15886  prodmolem2a  15907  zprod  15910  fprod  15914  pcmptdvds  16872  prdsdsval2  17454  gsumconstf  19872  gsummpt1n0  19902  gsum2d2  19911  dprd2d2  19983  gsumdixp  20235  psrass1lem  21848  coe1fzgsumdlem  22197  gsumply1eq  22203  evl1gsumdlem  22250  madugsum  22537  cnmpt1t  23559  cnmpt2k  23582  elmptrab  23721  flfcnp2  23901  prdsxmet  24264  fsumcn  24768  ovoliunlem3  25412  ovoliun  25413  ovoliun2  25414  voliun  25462  mbfpos  25559  mbfposb  25561  i1fposd  25615  itg2cnlem1  25669  isibl2  25674  cbvitg  25684  itgss3  25723  itgfsum  25735  itgabs  25743  itgcn  25753  limcmpt  25791  dvmptfsum  25886  lhop2  25927  dvfsumle  25933  dvfsumleOLD  25934  dvfsumlem2  25940  dvfsumlem2OLD  25941  itgsubstlem  25962  itgsubst  25963  itgulm2  26325  rlimcnp2  26883  gsummpt2co  32995  gsumpart  33004  esumsnf  34061  mbfposadd  37668  itgabsnc  37690  ftc1cnnclem  37692  ftc2nc  37703  zndvdchrrhm  41967  aks6d1c1  42111  evl1gprodd  42112  aks6d1c2  42125  idomnnzgmulnz  42128  deg1gprod  42135  sticksstones12a  42152  aks6d1c6lem5  42172  aks6d1c7lem2  42176  aks6d1c7lem3  42177  aks5lem4a  42185  mzpsubst  42743  rabdiophlem2  42797  aomclem8  43057  fsumcnf  45022  disjf1  45184  disjrnmpt2  45189  disjinfi  45193  fmptf  45240  cncfmptss  45592  mulc1cncfg  45594  expcnfg  45596  fprodcn  45605  fnlimabslt  45684  climmptf  45686  liminfvalxr  45788  liminfpnfuz  45821  xlimpnfxnegmnf2  45863  icccncfext  45892  cncficcgt0  45893  cncfiooicclem1  45898  fprodcncf  45905  dvmptmulf  45942  iblsplitf  45975  stoweidlem21  46026  stirlinglem4  46082  stirlinglem13  46091  stirlinglem15  46093  fourierd  46227  fourierclimd  46228  sge0iunmptlemre  46420  sge0iunmpt  46423  sge0ltfirpmpt2  46431  sge0isummpt2  46437  sge0xaddlem2  46439  sge0xadd  46440  meadjiun  46471  meaiunincf  46488  meaiuninc3  46490  omeiunle  46522  caratheodorylem2  46532  ovncvrrp  46569  vonioo  46687  smflim2  46811  smfsup  46819  smfinf  46823  smflimsup  46833  smfliminf  46836