Theorem cbvmpt 5201

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

Syntax hints:   → wi 4   = wceq 1542  Ⅎwnfc 2884   ↦ cmpt 5180

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-opab 5162  df-mpt 5181

This theorem is referenced by:  dffn5f  6906  fvmpts  6946  fvmpt2i  6953  fvmptex  6957  fmptcof  7077  fmptcos  7078  fliftfuns  7262  offval2  7644  ofmpteq  7647  mpocurryvald  8214  qliftfuns  8745  axcc2  10351  seqof2  13987  summolem2a  15642  zsum  15645  fsumcvg2  15654  fsumrlim  15738  cbvprod  15840  prodmolem2a  15861  zprod  15864  fprod  15868  pcmptdvds  16826  prdsdsval2  17408  gsumconstf  19868  gsummpt1n0  19898  gsum2d2  19907  dprd2d2  19979  gsumdixp  20258  psrass1lem  21892  coe1fzgsumdlem  22251  gsumply1eq  22257  evl1gsumdlem  22304  madugsum  22591  cnmpt1t  23613  cnmpt2k  23636  elmptrab  23775  flfcnp2  23955  prdsxmet  24317  fsumcn  24821  ovoliunlem3  25465  ovoliun  25466  ovoliun2  25467  voliun  25515  mbfpos  25612  mbfposb  25614  i1fposd  25668  itg2cnlem1  25722  isibl2  25727  cbvitg  25737  itgss3  25776  itgfsum  25788  itgabs  25796  itgcn  25806  limcmpt  25844  dvmptfsum  25939  lhop2  25980  dvfsumle  25986  dvfsumleOLD  25987  dvfsumlem2  25993  dvfsumlem2OLD  25994  itgsubstlem  26015  itgsubst  26016  itgulm2  26378  rlimcnp2  26936  gsummpt2co  33112  gsumpart  33127  esumsnf  34202  mbfposadd  37839  itgabsnc  37861  ftc1cnnclem  37863  ftc2nc  37874  zndvdchrrhm  42263  aks6d1c1  42407  evl1gprodd  42408  aks6d1c2  42421  idomnnzgmulnz  42424  deg1gprod  42431  sticksstones12a  42448  aks6d1c6lem5  42468  aks6d1c7lem2  42472  aks6d1c7lem3  42473  aks5lem4a  42481  mzpsubst  43026  rabdiophlem2  43080  aomclem8  43339  fsumcnf  45302  disjf1  45463  disjrnmpt2  45468  disjinfi  45472  fmptf  45519  cncfmptss  45869  mulc1cncfg  45871  expcnfg  45873  fprodcn  45882  fnlimabslt  45959  climmptf  45961  liminfvalxr  46063  liminfpnfuz  46096  xlimpnfxnegmnf2  46138  icccncfext  46167  cncficcgt0  46168  cncfiooicclem1  46173  fprodcncf  46180  dvmptmulf  46217  iblsplitf  46250  stoweidlem21  46301  stirlinglem4  46357  stirlinglem13  46366  stirlinglem15  46368  fourierd  46502  fourierclimd  46503  sge0iunmptlemre  46695  sge0iunmpt  46698  sge0ltfirpmpt2  46706  sge0isummpt2  46712  sge0xaddlem2  46714  sge0xadd  46715  meadjiun  46746  meaiunincf  46763  meaiuninc3  46765  omeiunle  46797  caratheodorylem2  46807  ovncvrrp  46844  vonioo  46962  smflim2  47086  smfsup  47094  smfinf  47098  smflimsup  47108  smfliminf  47111