Theorem cbvmpt 5188

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

Syntax hints:   → wi 4   = wceq 1542  Ⅎwnfc 2884   ↦ cmpt 5167

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149  df-mpt 5168

This theorem is referenced by:  dffn5f  6903  fvmpts  6943  fvmpt2i  6950  fvmptex  6954  fmptcof  7075  fmptcos  7076  fliftfuns  7260  offval2  7642  ofmpteq  7645  mpocurryvald  8211  qliftfuns  8742  axcc2  10348  seqof2  14011  summolem2a  15666  zsum  15669  fsumcvg2  15678  fsumrlim  15763  cbvprod  15867  prodmolem2a  15888  zprod  15891  fprod  15895  pcmptdvds  16854  prdsdsval2  17436  gsumconstf  19899  gsummpt1n0  19929  gsum2d2  19938  dprd2d2  20010  gsumdixp  20287  psrass1lem  21920  coe1fzgsumdlem  22277  gsumply1eq  22283  evl1gsumdlem  22330  madugsum  22617  cnmpt1t  23639  cnmpt2k  23662  elmptrab  23801  flfcnp2  23981  prdsxmet  24343  fsumcn  24846  ovoliunlem3  25480  ovoliun  25481  ovoliun2  25482  voliun  25530  mbfpos  25627  mbfposb  25629  i1fposd  25683  itg2cnlem1  25737  isibl2  25742  cbvitg  25752  itgss3  25791  itgfsum  25803  itgabs  25811  itgcn  25821  limcmpt  25859  dvmptfsum  25951  lhop2  25992  dvfsumle  25998  dvfsumleOLD  25999  dvfsumlem2  26005  dvfsumlem2OLD  26006  itgsubstlem  26027  itgsubst  26028  itgulm2  26389  rlimcnp2  26947  gsummpt2co  33129  gsumpart  33144  esumsnf  34229  mbfposadd  37999  itgabsnc  38021  ftc1cnnclem  38023  ftc2nc  38034  zndvdchrrhm  42423  aks6d1c1  42566  evl1gprodd  42567  aks6d1c2  42580  idomnnzgmulnz  42583  deg1gprod  42590  sticksstones12a  42607  aks6d1c6lem5  42627  aks6d1c7lem2  42631  aks6d1c7lem3  42632  aks5lem4a  42640  mzpsubst  43191  rabdiophlem2  43245  aomclem8  43504  fsumcnf  45467  disjf1  45628  disjrnmpt2  45633  disjinfi  45637  fmptf  45683  cncfmptss  46032  mulc1cncfg  46034  expcnfg  46036  fprodcn  46045  fnlimabslt  46122  climmptf  46124  liminfvalxr  46226  liminfpnfuz  46259  xlimpnfxnegmnf2  46301  icccncfext  46330  cncficcgt0  46331  cncfiooicclem1  46336  fprodcncf  46343  dvmptmulf  46380  iblsplitf  46413  stoweidlem21  46464  stirlinglem4  46520  stirlinglem13  46529  stirlinglem15  46531  fourierd  46665  fourierclimd  46666  sge0iunmptlemre  46858  sge0iunmpt  46861  sge0ltfirpmpt2  46869  sge0isummpt2  46875  sge0xaddlem2  46877  sge0xadd  46878  meadjiun  46909  meaiunincf  46926  meaiuninc3  46928  omeiunle  46960  caratheodorylem2  46970  ovncvrrp  47007  vonioo  47125  smflim2  47249  smfsup  47257  smfinf  47261  smflimsup  47271  smfliminf  47274