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 1570  Ⅎwnfc 2907   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  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  6944  fvmpts  6985  fvmpt2i  6992  fvmptex  6996  fmptcof  7119  fmptcos  7120  fliftfuns  7310  offval2  7696  ofmpteq  7699  mpocurryvald  8265  qliftfuns  8803  axcc2  10487  seqof2  14172  summolem2a  15849  zsum  15852  fsumcvg2  15861  fsumrlim  15946  cbvprod  16050  prodmolem2a  16069  zprod  16072  fprod  16076  pcmptdvds  17034  prdsdsval2  17617  gsumconstf  20111  gsummpt1n0  20141  gsum2d2  20150  dprd2d2  20222  gsumdixp  20510  psrass1lem  22203  coe1fzgsumdlem  22583  gsumply1eq  22589  evl1gsumdlem  22636  madugsum  22920  cnmpt1t  23946  cnmpt2k  23969  elmptrab  24108  flfcnp2  24288  prdsxmet  24650  fsumcn  25153  ovoliunlem3  25787  ovoliun  25788  ovoliun2  25789  voliun  25837  mbfpos  25934  mbfposb  25936  i1fposd  25990  itg2cnlem1  26044  isibl2  26049  cbvitg  26058  itgss3  26097  itgfsum  26109  itgabs  26117  itgcn  26127  limcmpt  26165  dvmptfsum  26257  lhop2  26297  dvfsumle  26303  dvfsumlem2  26309  itgsubstlem  26330  itgsubst  26331  itgulm2  26700  rlimcnp2  27258  gsummpt2co  33543  gsumpart  33558  esumsnf  34630  mbfposadd  38505  itgabsnc  38527  ftc1cnnclem  38529  ftc2nc  38540  zndvdchrrhm  42943  aks6d1c1  43086  evl1gprodd  43087  aks6d1c2  43100  idomnnzgmulnz  43103  deg1gprod  43110  sticksstones12a  43127  aks6d1c6lem5  43147  aks6d1c7lem2  43151  aks6d1c7lem3  43152  aks5lem4a  43160  mzpsubst  43697  rabdiophlem2  43747  aomclem8  44006  fsumcnf  45959  disjf1  46119  disjrnmpt2  46124  disjinfi  46128  fmptf  46172  cncfmptss  46521  mulc1cncfg  46523  expcnfg  46525  fprodcn  46534  fnlimabslt  46611  climmptf  46613  liminfvalxr  46715  liminfpnfuz  46748  xlimpnfxnegmnf2  46790  icccncfext  46819  cncficcgt0  46820  cncfiooicclem1  46825  fprodcncf  46832  dvmptmulf  46869  iblsplitf  46902  stoweidlem21  46953  stirlinglem4  47009  stirlinglem13  47018  stirlinglem15  47020  fourierd  47154  fourierclimd  47155  sge0iunmptlemre  47347  sge0iunmpt  47350  sge0ltfirpmpt2  47358  sge0isummpt2  47364  sge0xaddlem2  47366  sge0xadd  47367  meadjiun  47398  meaiunincf  47415  meaiuninc3  47417  omeiunle  47449  caratheodorylem2  47459  ovncvrrp  47496  vonioo  47614  smflim2  47738  smfsup  47746  smfinf  47750  smflimsup  47760  smfliminf  47763