Theorem cbvmpt 5206

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  Ⅎwnfc 2907   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-opab 5167  df-mpt 5186

This theorem is used by:  dffn5f  6956  fvmpts  6997  fvmpt2i  7004  fvmptex  7008  fmptcof  7131  fmptcos  7132  fliftfuns  7322  offval2  7713  ofmpteq  7716  mpocurryvald  8288  qliftfuns  8826  axcc2  10516  seqof2  14204  summolem2a  15882  zsum  15885  fsumcvg2  15894  fsumrlim  15979  cbvprod  16083  prodmolem2a  16102  zprod  16105  fprod  16109  pcmptdvds  17073  prdsdsval2  17656  gsumconstf  20150  gsummpt1n0  20180  gsum2d2  20189  dprd2d2  20261  gsumdixp  20549  psrass1lem  22242  coe1fzgsumdlem  22622  gsumply1eq  22628  evl1gsumdlem  22675  madugsum  22959  cnmpt1t  23985  cnmpt2k  24008  elmptrab  24147  flfcnp2  24327  prdsxmet  24689  fsumcn  25192  ovoliunlem3  25826  ovoliun  25827  ovoliun2  25828  voliun  25876  mbfpos  25973  mbfposb  25975  i1fposd  26029  itg2cnlem1  26083  isibl2  26088  cbvitg  26097  itgss3  26136  itgfsum  26148  itgabs  26156  itgcn  26166  limcmpt  26204  dvmptfsum  26296  lhop2  26336  dvfsumle  26342  dvfsumlem2  26348  itgsubstlem  26369  itgsubst  26370  itgulm2  26737  rlimcnp2  27295  gsummpt2co  33652  gsumpart  33667  esumsnf  34739  mbfposadd  38661  itgabsnc  38683  ftc1cnnclem  38685  ftc2nc  38696  zndvdchrrhm  43099  aks6d1c1  43242  evl1gprodd  43243  aks6d1c2  43256  idomnnzgmulnz  43259  deg1gprod  43266  sticksstones12a  43283  aks6d1c6lem5  43303  aks6d1c7lem2  43307  aks6d1c7lem3  43308  aks5lem4a  43316  mzpsubst  43835  rabdiophlem2  43885  aomclem8  44139  fsumcnf  46114  disjf1  46274  disjrnmpt2  46279  disjinfi  46283  fmptf  46327  cncfmptss  46675  mulc1cncfg  46677  expcnfg  46679  fprodcn  46688  fnlimabslt  46765  climmptf  46767  liminfvalxr  46869  liminfpnfuz  46902  xlimpnfxnegmnf2  46944  icccncfext  46973  cncficcgt0  46974  cncfiooicclem1  46979  fprodcncf  46986  dvmptmulf  47023  iblsplitf  47056  stoweidlem21  47107  stirlinglem4  47163  stirlinglem13  47172  stirlinglem15  47174  fourierd  47308  fourierclimd  47309  sge0iunmptlemre  47501  sge0iunmpt  47504  sge0ltfirpmpt2  47512  sge0isummpt2  47518  sge0xaddlem2  47520  sge0xadd  47521  meadjiun  47552  meaiunincf  47569  meaiuninc3  47571  omeiunle  47603  caratheodorylem2  47613  ovncvrrp  47650  vonioo  47768  smflim2  47892  smfsup  47900  smfinf  47904  smflimsup  47914  smfliminf  47917