Theorem cbvmpt 5191

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

Syntax hints:   → wi 4   = wceq 1541  Ⅎwnfc 2877   ↦ cmpt 5170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-opab 5152  df-mpt 5171

This theorem is referenced by:  dffn5f  6888  fvmpts  6927  fvmpt2i  6934  fvmptex  6938  fmptcof  7058  fmptcos  7059  fliftfuns  7243  offval2  7625  ofmpteq  7628  mpocurryvald  8195  qliftfuns  8723  axcc2  10320  seqof2  13959  summolem2a  15614  zsum  15617  fsumcvg2  15626  fsumrlim  15710  cbvprod  15812  prodmolem2a  15833  zprod  15836  fprod  15840  pcmptdvds  16798  prdsdsval2  17380  gsumconstf  19840  gsummpt1n0  19870  gsum2d2  19879  dprd2d2  19951  gsumdixp  20230  psrass1lem  21862  coe1fzgsumdlem  22211  gsumply1eq  22217  evl1gsumdlem  22264  madugsum  22551  cnmpt1t  23573  cnmpt2k  23596  elmptrab  23735  flfcnp2  23915  prdsxmet  24277  fsumcn  24781  ovoliunlem3  25425  ovoliun  25426  ovoliun2  25427  voliun  25475  mbfpos  25572  mbfposb  25574  i1fposd  25628  itg2cnlem1  25682  isibl2  25687  cbvitg  25697  itgss3  25736  itgfsum  25748  itgabs  25756  itgcn  25766  limcmpt  25804  dvmptfsum  25899  lhop2  25940  dvfsumle  25946  dvfsumleOLD  25947  dvfsumlem2  25953  dvfsumlem2OLD  25954  itgsubstlem  25975  itgsubst  25976  itgulm2  26338  rlimcnp2  26896  gsummpt2co  33018  gsumpart  33027  esumsnf  34067  mbfposadd  37686  itgabsnc  37708  ftc1cnnclem  37710  ftc2nc  37721  zndvdchrrhm  41984  aks6d1c1  42128  evl1gprodd  42129  aks6d1c2  42142  idomnnzgmulnz  42145  deg1gprod  42152  sticksstones12a  42169  aks6d1c6lem5  42189  aks6d1c7lem2  42193  aks6d1c7lem3  42194  aks5lem4a  42202  mzpsubst  42760  rabdiophlem2  42814  aomclem8  43073  fsumcnf  45037  disjf1  45199  disjrnmpt2  45204  disjinfi  45208  fmptf  45255  cncfmptss  45606  mulc1cncfg  45608  expcnfg  45610  fprodcn  45619  fnlimabslt  45696  climmptf  45698  liminfvalxr  45800  liminfpnfuz  45833  xlimpnfxnegmnf2  45875  icccncfext  45904  cncficcgt0  45905  cncfiooicclem1  45910  fprodcncf  45917  dvmptmulf  45954  iblsplitf  45987  stoweidlem21  46038  stirlinglem4  46094  stirlinglem13  46103  stirlinglem15  46105  fourierd  46239  fourierclimd  46240  sge0iunmptlemre  46432  sge0iunmpt  46435  sge0ltfirpmpt2  46443  sge0isummpt2  46449  sge0xaddlem2  46451  sge0xadd  46452  meadjiun  46483  meaiunincf  46500  meaiuninc3  46502  omeiunle  46534  caratheodorylem2  46544  ovncvrrp  46581  vonioo  46699  smflim2  46823  smfsup  46831  smfinf  46835  smflimsup  46845  smfliminf  46848