Theorem cbvmpt 5209

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

Syntax hints:   → wi 4   = wceq 1540  Ⅎwnfc 2876   ↦ cmpt 5188

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5170  df-mpt 5189

This theorem is referenced by:  dffn5f  6932  fvmpts  6971  fvmpt2i  6978  fvmptex  6982  fmptcof  7102  fmptcos  7103  fliftfuns  7289  offval2  7673  ofmpteq  7676  mpocurryvald  8249  qliftfuns  8777  axcc2  10390  seqof2  14025  summolem2a  15681  zsum  15684  fsumcvg2  15693  fsumrlim  15777  cbvprod  15879  prodmolem2a  15900  zprod  15903  fprod  15907  pcmptdvds  16865  prdsdsval2  17447  gsumconstf  19865  gsummpt1n0  19895  gsum2d2  19904  dprd2d2  19976  gsumdixp  20228  psrass1lem  21841  coe1fzgsumdlem  22190  gsumply1eq  22196  evl1gsumdlem  22243  madugsum  22530  cnmpt1t  23552  cnmpt2k  23575  elmptrab  23714  flfcnp2  23894  prdsxmet  24257  fsumcn  24761  ovoliunlem3  25405  ovoliun  25406  ovoliun2  25407  voliun  25455  mbfpos  25552  mbfposb  25554  i1fposd  25608  itg2cnlem1  25662  isibl2  25667  cbvitg  25677  itgss3  25716  itgfsum  25728  itgabs  25736  itgcn  25746  limcmpt  25784  dvmptfsum  25879  lhop2  25920  dvfsumle  25926  dvfsumleOLD  25927  dvfsumlem2  25933  dvfsumlem2OLD  25934  itgsubstlem  25955  itgsubst  25956  itgulm2  26318  rlimcnp2  26876  gsummpt2co  32988  gsumpart  32997  esumsnf  34054  mbfposadd  37661  itgabsnc  37683  ftc1cnnclem  37685  ftc2nc  37696  zndvdchrrhm  41960  aks6d1c1  42104  evl1gprodd  42105  aks6d1c2  42118  idomnnzgmulnz  42121  deg1gprod  42128  sticksstones12a  42145  aks6d1c6lem5  42165  aks6d1c7lem2  42169  aks6d1c7lem3  42170  aks5lem4a  42178  mzpsubst  42736  rabdiophlem2  42790  aomclem8  43050  fsumcnf  45015  disjf1  45177  disjrnmpt2  45182  disjinfi  45186  fmptf  45233  cncfmptss  45585  mulc1cncfg  45587  expcnfg  45589  fprodcn  45598  fnlimabslt  45677  climmptf  45679  liminfvalxr  45781  liminfpnfuz  45814  xlimpnfxnegmnf2  45856  icccncfext  45885  cncficcgt0  45886  cncfiooicclem1  45891  fprodcncf  45898  dvmptmulf  45935  iblsplitf  45968  stoweidlem21  46019  stirlinglem4  46075  stirlinglem13  46084  stirlinglem15  46086  fourierd  46220  fourierclimd  46221  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0ltfirpmpt2  46424  sge0isummpt2  46430  sge0xaddlem2  46432  sge0xadd  46433  meadjiun  46464  meaiunincf  46481  meaiuninc3  46483  omeiunle  46515  caratheodorylem2  46525  ovncvrrp  46562  vonioo  46680  smflim2  46804  smfsup  46812  smfinf  46816  smflimsup  46826  smfliminf  46829