Theorem cbvmpt 5258

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 2369. See cbvmptg 5259 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 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 2901	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2901	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvmpt.1	. 2 ⊢ Ⅎ𝑦𝐵
4		cbvmpt.2	. 2 ⊢ Ⅎ𝑥𝐶
5		cbvmpt.3	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
6	1, 2, 3, 4, 5	cbvmptf 5256	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1539  Ⅎwnfc 2881   ↦ cmpt 5230

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-opab 5210  df-mpt 5231

This theorem is referenced by:  cbvmptvOLD  5261  dffn5f  6962  fvmpts  7000  fvmpt2i  7007  fvmptex  7011  fmptcof  7129  fmptcos  7130  fliftfuns  7313  offval2  7692  ofmpteq  7694  mpocurryvald  8257  qliftfuns  8800  axcc2  10434  seqof2  14030  summolem2a  15665  zsum  15668  fsumcvg2  15677  fsumrlim  15761  cbvprod  15863  prodmolem2a  15882  zprod  15885  fprod  15889  pcmptdvds  16831  prdsdsval2  17434  gsumconstf  19844  gsummpt1n0  19874  gsum2d2  19883  dprd2d2  19955  gsumdixp  20207  psrass1lemOLD  21712  psrass1lem  21715  coe1fzgsumdlem  22045  gsumply1eq  22049  evl1gsumdlem  22095  madugsum  22365  cnmpt1t  23389  cnmpt2k  23412  elmptrab  23551  flfcnp2  23731  prdsxmet  24095  fsumcn  24608  ovoliunlem3  25253  ovoliun  25254  ovoliun2  25255  voliun  25303  mbfpos  25400  mbfposb  25402  i1fposd  25457  itg2cnlem1  25511  isibl2  25516  cbvitg  25525  itgss3  25564  itgfsum  25576  itgabs  25584  itgcn  25594  limcmpt  25632  dvmptfsum  25727  lhop2  25767  dvfsumle  25773  dvfsumlem2  25779  itgsubstlem  25800  itgsubst  25801  itgulm2  26157  rlimcnp2  26707  gsummpt2co  32470  gsumpart  32477  esumsnf  33360  gg-dvfsumle  35468  gg-dvfsumlem2  35469  mbfposadd  36838  itgabsnc  36860  ftc1cnnclem  36862  ftc2nc  36873  sticksstones12a  41279  mzpsubst  41788  rabdiophlem2  41842  aomclem8  42105  fsumcnf  44007  disjf1  44180  disjrnmpt2  44185  disjinfi  44189  fmptf  44240  cncfmptss  44601  mulc1cncfg  44603  expcnfg  44605  fprodcn  44614  fnlimabslt  44693  climmptf  44695  liminfvalxr  44797  liminfpnfuz  44830  xlimpnfxnegmnf2  44872  icccncfext  44901  cncficcgt0  44902  cncfiooicclem1  44907  fprodcncf  44914  dvmptmulf  44951  iblsplitf  44984  stoweidlem21  45035  stirlinglem4  45091  stirlinglem13  45100  stirlinglem15  45102  fourierd  45236  fourierclimd  45237  sge0iunmptlemre  45429  sge0iunmpt  45432  sge0ltfirpmpt2  45440  sge0isummpt2  45446  sge0xaddlem2  45448  sge0xadd  45449  meadjiun  45480  meaiunincf  45497  meaiuninc3  45499  omeiunle  45531  caratheodorylem2  45541  ovncvrrp  45578  vonioo  45696  smflim2  45820  smfsup  45828  smfinf  45832  smflimsup  45842  smfliminf  45845