Theorem cbvmpt 5185

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

Syntax hints:   → wi 4   = wceq 1539  Ⅎwnfc 2887   ↦ cmpt 5157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5137  df-mpt 5158

This theorem is referenced by:  cbvmptvOLD  5188  dffn5f  6840  fvmpts  6878  fvmpt2i  6885  fvmptex  6889  fmptcof  7002  fmptcos  7003  fliftfuns  7185  offval2  7553  ofmpteq  7555  mpocurryvald  8086  qliftfuns  8593  axcc2  10193  seqof2  13781  summolem2a  15427  zsum  15430  fsumcvg2  15439  fsumrlim  15523  cbvprod  15625  prodmolem2a  15644  zprod  15647  fprod  15651  pcmptdvds  16595  prdsdsval2  17195  gsumconstf  19536  gsummpt1n0  19566  gsum2d2  19575  dprd2d2  19647  gsumdixp  19848  psrass1lemOLD  21143  psrass1lem  21146  coe1fzgsumdlem  21472  gsumply1eq  21476  evl1gsumdlem  21522  madugsum  21792  cnmpt1t  22816  cnmpt2k  22839  elmptrab  22978  flfcnp2  23158  prdsxmet  23522  fsumcn  24033  ovoliunlem3  24668  ovoliun  24669  ovoliun2  24670  voliun  24718  mbfpos  24815  mbfposb  24817  i1fposd  24872  itg2cnlem1  24926  isibl2  24931  cbvitg  24940  itgss3  24979  itgfsum  24991  itgabs  24999  itgcn  25009  limcmpt  25047  dvmptfsum  25139  lhop2  25179  dvfsumle  25185  dvfsumlem2  25191  itgsubstlem  25212  itgsubst  25213  itgulm2  25568  rlimcnp2  26116  gsummpt2co  31308  gsumpart  31315  esumsnf  32032  mbfposadd  35824  itgabsnc  35846  ftc1cnnclem  35848  ftc2nc  35859  sticksstones12a  40113  mzpsubst  40570  rabdiophlem2  40624  aomclem8  40886  fsumcnf  42564  disjf1  42720  disjrnmpt2  42726  disjinfi  42731  fmptf  42783  cncfmptss  43128  mulc1cncfg  43130  expcnfg  43132  fprodcn  43141  fnlimabslt  43220  climmptf  43222  liminfvalxr  43324  liminfpnfuz  43357  xlimpnfxnegmnf2  43399  icccncfext  43428  cncficcgt0  43429  cncfiooicclem1  43434  fprodcncf  43441  dvmptmulf  43478  iblsplitf  43511  stoweidlem21  43562  stirlinglem4  43618  stirlinglem13  43627  stirlinglem15  43629  fourierd  43763  fourierclimd  43764  sge0iunmptlemre  43953  sge0iunmpt  43956  sge0ltfirpmpt2  43964  sge0isummpt2  43970  sge0xaddlem2  43972  sge0xadd  43973  meadjiun  44004  meaiunincf  44021  meaiuninc3  44023  omeiunle  44055  caratheodorylem2  44065  ovncvrrp  44102  vonioo  44220  smflim2  44339  smfsup  44347  smfinf  44351  smflimsup  44361  smfliminf  44364