Theorem cbvmpt 5259

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

Syntax hints:   → wi 4   = wceq 1541  Ⅎwnfc 2883   ↦ cmpt 5231

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-opab 5211  df-mpt 5232

This theorem is referenced by:  cbvmptvOLD  5262  dffn5f  6963  fvmpts  7001  fvmpt2i  7008  fvmptex  7012  fmptcof  7127  fmptcos  7128  fliftfuns  7310  offval2  7689  ofmpteq  7691  mpocurryvald  8254  qliftfuns  8797  axcc2  10431  seqof2  14025  summolem2a  15660  zsum  15663  fsumcvg2  15672  fsumrlim  15756  cbvprod  15858  prodmolem2a  15877  zprod  15880  fprod  15884  pcmptdvds  16826  prdsdsval2  17429  gsumconstf  19802  gsummpt1n0  19832  gsum2d2  19841  dprd2d2  19913  gsumdixp  20130  psrass1lemOLD  21492  psrass1lem  21495  coe1fzgsumdlem  21824  gsumply1eq  21828  evl1gsumdlem  21874  madugsum  22144  cnmpt1t  23168  cnmpt2k  23191  elmptrab  23330  flfcnp2  23510  prdsxmet  23874  fsumcn  24385  ovoliunlem3  25020  ovoliun  25021  ovoliun2  25022  voliun  25070  mbfpos  25167  mbfposb  25169  i1fposd  25224  itg2cnlem1  25278  isibl2  25283  cbvitg  25292  itgss3  25331  itgfsum  25343  itgabs  25351  itgcn  25361  limcmpt  25399  dvmptfsum  25491  lhop2  25531  dvfsumle  25537  dvfsumlem2  25543  itgsubstlem  25564  itgsubst  25565  itgulm2  25920  rlimcnp2  26468  gsummpt2co  32195  gsumpart  32202  esumsnf  33057  gg-dvfsumle  35177  gg-dvfsumlem2  35178  mbfposadd  36530  itgabsnc  36552  ftc1cnnclem  36554  ftc2nc  36565  sticksstones12a  40968  mzpsubst  41476  rabdiophlem2  41530  aomclem8  41793  fsumcnf  43695  disjf1  43870  disjrnmpt2  43876  disjinfi  43881  fmptf  43932  cncfmptss  44293  mulc1cncfg  44295  expcnfg  44297  fprodcn  44306  fnlimabslt  44385  climmptf  44387  liminfvalxr  44489  liminfpnfuz  44522  xlimpnfxnegmnf2  44564  icccncfext  44593  cncficcgt0  44594  cncfiooicclem1  44599  fprodcncf  44606  dvmptmulf  44643  iblsplitf  44676  stoweidlem21  44727  stirlinglem4  44783  stirlinglem13  44792  stirlinglem15  44794  fourierd  44928  fourierclimd  44929  sge0iunmptlemre  45121  sge0iunmpt  45124  sge0ltfirpmpt2  45132  sge0isummpt2  45138  sge0xaddlem2  45140  sge0xadd  45141  meadjiun  45172  meaiunincf  45189  meaiuninc3  45191  omeiunle  45223  caratheodorylem2  45233  ovncvrrp  45270  vonioo  45388  smflim2  45512  smfsup  45520  smfinf  45524  smflimsup  45534  smfliminf  45537