Theorem cbvmpt 5211

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

Syntax hints:   → wi 4   = wceq 1540  Ⅎwnfc 2877   ↦ cmpt 5190

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5172  df-mpt 5191

This theorem is referenced by:  dffn5f  6934  fvmpts  6973  fvmpt2i  6980  fvmptex  6984  fmptcof  7104  fmptcos  7105  fliftfuns  7291  offval2  7675  ofmpteq  7678  mpocurryvald  8251  qliftfuns  8779  axcc2  10396  seqof2  14031  summolem2a  15687  zsum  15690  fsumcvg2  15699  fsumrlim  15783  cbvprod  15885  prodmolem2a  15906  zprod  15909  fprod  15913  pcmptdvds  16871  prdsdsval2  17453  gsumconstf  19871  gsummpt1n0  19901  gsum2d2  19910  dprd2d2  19982  gsumdixp  20234  psrass1lem  21847  coe1fzgsumdlem  22196  gsumply1eq  22202  evl1gsumdlem  22249  madugsum  22536  cnmpt1t  23558  cnmpt2k  23581  elmptrab  23720  flfcnp2  23900  prdsxmet  24263  fsumcn  24767  ovoliunlem3  25411  ovoliun  25412  ovoliun2  25413  voliun  25461  mbfpos  25558  mbfposb  25560  i1fposd  25614  itg2cnlem1  25668  isibl2  25673  cbvitg  25683  itgss3  25722  itgfsum  25734  itgabs  25742  itgcn  25752  limcmpt  25790  dvmptfsum  25885  lhop2  25926  dvfsumle  25932  dvfsumleOLD  25933  dvfsumlem2  25939  dvfsumlem2OLD  25940  itgsubstlem  25961  itgsubst  25962  itgulm2  26324  rlimcnp2  26882  gsummpt2co  32994  gsumpart  33003  esumsnf  34060  mbfposadd  37656  itgabsnc  37678  ftc1cnnclem  37680  ftc2nc  37691  zndvdchrrhm  41955  aks6d1c1  42099  evl1gprodd  42100  aks6d1c2  42113  idomnnzgmulnz  42116  deg1gprod  42123  sticksstones12a  42140  aks6d1c6lem5  42160  aks6d1c7lem2  42164  aks6d1c7lem3  42165  aks5lem4a  42173  mzpsubst  42729  rabdiophlem2  42783  aomclem8  43043  fsumcnf  45008  disjf1  45170  disjrnmpt2  45175  disjinfi  45179  fmptf  45226  cncfmptss  45578  mulc1cncfg  45580  expcnfg  45582  fprodcn  45591  fnlimabslt  45670  climmptf  45672  liminfvalxr  45774  liminfpnfuz  45807  xlimpnfxnegmnf2  45849  icccncfext  45878  cncficcgt0  45879  cncfiooicclem1  45884  fprodcncf  45891  dvmptmulf  45928  iblsplitf  45961  stoweidlem21  46012  stirlinglem4  46068  stirlinglem13  46077  stirlinglem15  46079  fourierd  46213  fourierclimd  46214  sge0iunmptlemre  46406  sge0iunmpt  46409  sge0ltfirpmpt2  46417  sge0isummpt2  46423  sge0xaddlem2  46425  sge0xadd  46426  meadjiun  46457  meaiunincf  46474  meaiuninc3  46476  omeiunle  46508  caratheodorylem2  46518  ovncvrrp  46555  vonioo  46673  smflim2  46797  smfsup  46805  smfinf  46809  smflimsup  46819  smfliminf  46822