Theorem cbvmpt 5202

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 5203 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 5200	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-mpt 5182

This theorem is referenced by:  dffn5f  6913  fvmpts  6953  fvmpt2i  6960  fvmptex  6964  fmptcof  7085  fmptcos  7086  fliftfuns  7270  offval2  7652  ofmpteq  7655  mpocurryvald  8222  qliftfuns  8753  axcc2  10359  seqof2  13995  summolem2a  15650  zsum  15653  fsumcvg2  15662  fsumrlim  15746  cbvprod  15848  prodmolem2a  15869  zprod  15872  fprod  15876  pcmptdvds  16834  prdsdsval2  17416  gsumconstf  19876  gsummpt1n0  19906  gsum2d2  19915  dprd2d2  19987  gsumdixp  20266  psrass1lem  21900  coe1fzgsumdlem  22259  gsumply1eq  22265  evl1gsumdlem  22312  madugsum  22599  cnmpt1t  23621  cnmpt2k  23644  elmptrab  23783  flfcnp2  23963  prdsxmet  24325  fsumcn  24829  ovoliunlem3  25473  ovoliun  25474  ovoliun2  25475  voliun  25523  mbfpos  25620  mbfposb  25622  i1fposd  25676  itg2cnlem1  25730  isibl2  25735  cbvitg  25745  itgss3  25784  itgfsum  25796  itgabs  25804  itgcn  25814  limcmpt  25852  dvmptfsum  25947  lhop2  25988  dvfsumle  25994  dvfsumleOLD  25995  dvfsumlem2  26001  dvfsumlem2OLD  26002  itgsubstlem  26023  itgsubst  26024  itgulm2  26386  rlimcnp2  26944  gsummpt2co  33141  gsumpart  33156  esumsnf  34241  mbfposadd  37907  itgabsnc  37929  ftc1cnnclem  37931  ftc2nc  37942  zndvdchrrhm  42331  aks6d1c1  42475  evl1gprodd  42476  aks6d1c2  42489  idomnnzgmulnz  42492  deg1gprod  42499  sticksstones12a  42516  aks6d1c6lem5  42536  aks6d1c7lem2  42540  aks6d1c7lem3  42541  aks5lem4a  42549  mzpsubst  43094  rabdiophlem2  43148  aomclem8  43407  fsumcnf  45370  disjf1  45531  disjrnmpt2  45536  disjinfi  45540  fmptf  45586  cncfmptss  45936  mulc1cncfg  45938  expcnfg  45940  fprodcn  45949  fnlimabslt  46026  climmptf  46028  liminfvalxr  46130  liminfpnfuz  46163  xlimpnfxnegmnf2  46205  icccncfext  46234  cncficcgt0  46235  cncfiooicclem1  46240  fprodcncf  46247  dvmptmulf  46284  iblsplitf  46317  stoweidlem21  46368  stirlinglem4  46424  stirlinglem13  46433  stirlinglem15  46435  fourierd  46569  fourierclimd  46570  sge0iunmptlemre  46762  sge0iunmpt  46765  sge0ltfirpmpt2  46773  sge0isummpt2  46779  sge0xaddlem2  46781  sge0xadd  46782  meadjiun  46813  meaiunincf  46830  meaiuninc3  46832  omeiunle  46864  caratheodorylem2  46874  ovncvrrp  46911  vonioo  47029  smflim2  47153  smfsup  47161  smfinf  47165  smflimsup  47175  smfliminf  47178