Theorem cbvmpt 5131

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

Syntax hints:   → wi 4   = wceq 1538  Ⅎwnfc 2936   ↦ cmpt 5110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-mpt 5111

This theorem is referenced by:  cbvmptv  5133  dffn5f  6711  fvmpts  6748  fvmpt2i  6755  fvmptex  6759  fmptcof  6869  fmptcos  6870  fliftfuns  7046  offval2  7406  ofmpteq  7408  mpocurryvald  7919  qliftfuns  8367  axcc2  9848  seqof2  13424  summolem2a  15064  zsum  15067  fsumcvg2  15076  fsumrlim  15158  cbvprod  15261  prodmolem2a  15280  zprod  15283  fprod  15287  pcmptdvds  16220  prdsdsval2  16749  gsumconstf  19048  gsummpt1n0  19078  gsum2d2  19087  dprd2d2  19159  gsumdixp  19355  psrass1lem  20615  coe1fzgsumdlem  20930  gsumply1eq  20934  evl1gsumdlem  20980  madugsum  21248  cnmpt1t  22270  cnmpt2k  22293  elmptrab  22432  flfcnp2  22612  prdsxmet  22976  fsumcn  23475  ovoliunlem3  24108  ovoliun  24109  ovoliun2  24110  voliun  24158  mbfpos  24255  mbfposb  24257  i1fposd  24311  itg2cnlem1  24365  isibl2  24370  cbvitg  24379  itgss3  24418  itgfsum  24430  itgabs  24438  itgcn  24448  limcmpt  24486  dvmptfsum  24578  lhop2  24618  dvfsumle  24624  dvfsumlem2  24630  itgsubstlem  24651  itgsubst  24652  itgulm2  25004  rlimcnp2  25552  gsummpt2co  30733  gsumpart  30740  esumsnf  31433  mbfposadd  35104  itgabsnc  35126  ftc1cnnclem  35128  ftc2nc  35139  mzpsubst  39689  rabdiophlem2  39743  aomclem8  40005  fsumcnf  41650  disjf1  41809  disjrnmpt2  41815  disjinfi  41820  fmptf  41875  cncfmptss  42229  mulc1cncfg  42231  expcnfg  42233  fprodcn  42242  fnlimabslt  42321  climmptf  42323  liminfvalxr  42425  liminfpnfuz  42458  xlimpnfxnegmnf2  42500  icccncfext  42529  cncficcgt0  42530  cncfiooicclem1  42535  fprodcncf  42542  dvmptmulf  42579  iblsplitf  42612  stoweidlem21  42663  stirlinglem4  42719  stirlinglem13  42728  stirlinglem15  42730  fourierd  42864  fourierclimd  42865  sge0iunmptlemre  43054  sge0iunmpt  43057  sge0ltfirpmpt2  43065  sge0isummpt2  43071  sge0xaddlem2  43073  sge0xadd  43074  meadjiun  43105  meaiunincf  43122  meaiuninc3  43124  omeiunle  43156  caratheodorylem2  43166  ovncvrrp  43203  vonioo  43321  smflim2  43437  smfsup  43445  smfinf  43449  smflimsup  43459  smfliminf  43462