Theorem cbvmpt 5197

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

Syntax hints:   → wi 4   = wceq 1541  Ⅎwnfc 2881   ↦ cmpt 5176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-opab 5158  df-mpt 5177

This theorem is referenced by:  dffn5f  6902  fvmpts  6941  fvmpt2i  6948  fvmptex  6952  fmptcof  7072  fmptcos  7073  fliftfuns  7257  offval2  7639  ofmpteq  7642  mpocurryvald  8209  qliftfuns  8737  axcc2  10338  seqof2  13977  summolem2a  15632  zsum  15635  fsumcvg2  15644  fsumrlim  15728  cbvprod  15830  prodmolem2a  15851  zprod  15854  fprod  15858  pcmptdvds  16816  prdsdsval2  17398  gsumconstf  19857  gsummpt1n0  19887  gsum2d2  19896  dprd2d2  19968  gsumdixp  20247  psrass1lem  21879  coe1fzgsumdlem  22228  gsumply1eq  22234  evl1gsumdlem  22281  madugsum  22568  cnmpt1t  23590  cnmpt2k  23613  elmptrab  23752  flfcnp2  23932  prdsxmet  24294  fsumcn  24798  ovoliunlem3  25442  ovoliun  25443  ovoliun2  25444  voliun  25492  mbfpos  25589  mbfposb  25591  i1fposd  25645  itg2cnlem1  25699  isibl2  25704  cbvitg  25714  itgss3  25753  itgfsum  25765  itgabs  25773  itgcn  25783  limcmpt  25821  dvmptfsum  25916  lhop2  25957  dvfsumle  25963  dvfsumleOLD  25964  dvfsumlem2  25970  dvfsumlem2OLD  25971  itgsubstlem  25992  itgsubst  25993  itgulm2  26355  rlimcnp2  26913  gsummpt2co  33039  gsumpart  33048  esumsnf  34088  mbfposadd  37717  itgabsnc  37739  ftc1cnnclem  37741  ftc2nc  37752  zndvdchrrhm  42075  aks6d1c1  42219  evl1gprodd  42220  aks6d1c2  42233  idomnnzgmulnz  42236  deg1gprod  42243  sticksstones12a  42260  aks6d1c6lem5  42280  aks6d1c7lem2  42284  aks6d1c7lem3  42285  aks5lem4a  42293  mzpsubst  42855  rabdiophlem2  42909  aomclem8  43168  fsumcnf  45132  disjf1  45294  disjrnmpt2  45299  disjinfi  45303  fmptf  45350  cncfmptss  45701  mulc1cncfg  45703  expcnfg  45705  fprodcn  45714  fnlimabslt  45791  climmptf  45793  liminfvalxr  45895  liminfpnfuz  45928  xlimpnfxnegmnf2  45970  icccncfext  45999  cncficcgt0  46000  cncfiooicclem1  46005  fprodcncf  46012  dvmptmulf  46049  iblsplitf  46082  stoweidlem21  46133  stirlinglem4  46189  stirlinglem13  46198  stirlinglem15  46200  fourierd  46334  fourierclimd  46335  sge0iunmptlemre  46527  sge0iunmpt  46530  sge0ltfirpmpt2  46538  sge0isummpt2  46544  sge0xaddlem2  46546  sge0xadd  46547  meadjiun  46578  meaiunincf  46595  meaiuninc3  46597  omeiunle  46629  caratheodorylem2  46639  ovncvrrp  46676  vonioo  46794  smflim2  46918  smfsup  46926  smfinf  46930  smflimsup  46940  smfliminf  46943