Theorem cbvmpt 5196

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

Syntax hints:   → wi 4   = wceq 1554  Ⅎwnfc 2903   ↦ cmpt 5175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-opab 5157  df-mpt 5176

This theorem is referenced by:  dffn5f  6927  fvmpts  6968  fvmpt2i  6975  fvmptex  6979  fmptcof  7101  fmptcos  7102  fliftfuns  7287  offval2  7669  ofmpteq  7672  mpocurryvald  8238  qliftfuns  8774  axcc2  10384  seqof2  14063  summolem2a  15718  zsum  15721  fsumcvg2  15730  fsumrlim  15815  cbvprod  15919  prodmolem2a  15940  zprod  15943  fprod  15947  pcmptdvds  16906  prdsdsval2  17489  gsumconstf  19951  gsummpt1n0  19981  gsum2d2  19990  dprd2d2  20062  gsumdixp  20339  psrass1lem  21958  coe1fzgsumdlem  22339  gsumply1eq  22345  evl1gsumdlem  22392  madugsum  22676  cnmpt1t  23698  cnmpt2k  23721  elmptrab  23860  flfcnp2  24040  prdsxmet  24402  fsumcn  24905  ovoliunlem3  25539  ovoliun  25540  ovoliun2  25541  voliun  25589  mbfpos  25686  mbfposb  25688  i1fposd  25742  itg2cnlem1  25796  isibl2  25801  cbvitg  25811  itgss3  25850  itgfsum  25862  itgabs  25870  itgcn  25880  limcmpt  25918  dvmptfsum  26010  lhop2  26050  dvfsumle  26056  dvfsumlem2  26062  itgsubstlem  26083  itgsubst  26084  itgulm2  26442  rlimcnp2  27001  gsummpt2co  33182  gsumpart  33197  esumsnf  34315  mbfposadd  38114  itgabsnc  38136  ftc1cnnclem  38138  ftc2nc  38149  zndvdchrrhm  42538  aks6d1c1  42681  evl1gprodd  42682  aks6d1c2  42695  idomnnzgmulnz  42698  deg1gprod  42705  sticksstones12a  42722  aks6d1c6lem5  42742  aks6d1c7lem2  42746  aks6d1c7lem3  42747  aks5lem4a  42755  mzpsubst  43277  rabdiophlem2  43327  aomclem8  43586  fsumcnf  45549  disjf1  45709  disjrnmpt2  45714  disjinfi  45718  fmptf  45762  cncfmptss  46111  mulc1cncfg  46113  expcnfg  46115  fprodcn  46124  fnlimabslt  46201  climmptf  46203  liminfvalxr  46305  liminfpnfuz  46338  xlimpnfxnegmnf2  46380  icccncfext  46409  cncficcgt0  46410  cncfiooicclem1  46415  fprodcncf  46422  dvmptmulf  46459  iblsplitf  46492  stoweidlem21  46543  stirlinglem4  46599  stirlinglem13  46608  stirlinglem15  46610  fourierd  46744  fourierclimd  46745  sge0iunmptlemre  46937  sge0iunmpt  46940  sge0ltfirpmpt2  46948  sge0isummpt2  46954  sge0xaddlem2  46956  sge0xadd  46957  meadjiun  46988  meaiunincf  47005  meaiuninc3  47007  omeiunle  47039  caratheodorylem2  47049  ovncvrrp  47086  vonioo  47204  smflim2  47328  smfsup  47336  smfinf  47340  smflimsup  47350  smfliminf  47353