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 2374. See cbvmptg 5259 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 2902	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2902	. 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 1536  Ⅎwnfc 2887   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-opab 5210  df-mpt 5231

This theorem is referenced by:  cbvmptvOLD  5261  dffn5f  6979  fvmpts  7018  fvmpt2i  7025  fvmptex  7029  fmptcof  7149  fmptcos  7150  fliftfuns  7333  offval2  7716  ofmpteq  7719  mpocurryvald  8293  qliftfuns  8842  axcc2  10474  seqof2  14097  summolem2a  15747  zsum  15750  fsumcvg2  15759  fsumrlim  15843  cbvprod  15945  prodmolem2a  15966  zprod  15969  fprod  15973  pcmptdvds  16927  prdsdsval2  17530  gsumconstf  19967  gsummpt1n0  19997  gsum2d2  20006  dprd2d2  20078  gsumdixp  20332  psrass1lem  21969  coe1fzgsumdlem  22322  gsumply1eq  22328  evl1gsumdlem  22375  madugsum  22664  cnmpt1t  23688  cnmpt2k  23711  elmptrab  23850  flfcnp2  24030  prdsxmet  24394  fsumcn  24907  ovoliunlem3  25552  ovoliun  25553  ovoliun2  25554  voliun  25602  mbfpos  25699  mbfposb  25701  i1fposd  25756  itg2cnlem1  25810  isibl2  25815  cbvitg  25825  itgss3  25864  itgfsum  25876  itgabs  25884  itgcn  25894  limcmpt  25932  dvmptfsum  26027  lhop2  26068  dvfsumle  26074  dvfsumleOLD  26075  dvfsumlem2  26081  dvfsumlem2OLD  26082  itgsubstlem  26103  itgsubst  26104  itgulm2  26466  rlimcnp2  27023  gsummpt2co  33033  gsumpart  33042  esumsnf  34044  mbfposadd  37653  itgabsnc  37675  ftc1cnnclem  37677  ftc2nc  37688  zndvdchrrhm  41952  aks6d1c1  42097  evl1gprodd  42098  aks6d1c2  42111  idomnnzgmulnz  42114  deg1gprod  42121  sticksstones12a  42138  aks6d1c6lem5  42158  aks6d1c7lem2  42162  aks6d1c7lem3  42163  aks5lem4a  42171  mzpsubst  42735  rabdiophlem2  42789  aomclem8  43049  fsumcnf  44958  disjf1  45125  disjrnmpt2  45130  disjinfi  45134  fmptf  45182  cncfmptss  45542  mulc1cncfg  45544  expcnfg  45546  fprodcn  45555  fnlimabslt  45634  climmptf  45636  liminfvalxr  45738  liminfpnfuz  45771  xlimpnfxnegmnf2  45813  icccncfext  45842  cncficcgt0  45843  cncfiooicclem1  45848  fprodcncf  45855  dvmptmulf  45892  iblsplitf  45925  stoweidlem21  45976  stirlinglem4  46032  stirlinglem13  46041  stirlinglem15  46043  fourierd  46177  fourierclimd  46178  sge0iunmptlemre  46370  sge0iunmpt  46373  sge0ltfirpmpt2  46381  sge0isummpt2  46387  sge0xaddlem2  46389  sge0xadd  46390  meadjiun  46421  meaiunincf  46438  meaiuninc3  46440  omeiunle  46472  caratheodorylem2  46482  ovncvrrp  46519  vonioo  46637  smflim2  46761  smfsup  46769  smfinf  46773  smflimsup  46783  smfliminf  46786