Theorem cbvmpt 5212

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

Syntax hints:   → wi 4   = wceq 1568  Ⅎwnfc 2908   ↦ cmpt 5191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-opab 5173  df-mpt 5192

This theorem is referenced by:  dffn5f  6952  fvmpts  6993  fvmpt2i  7000  fvmptex  7004  fmptcof  7126  fmptcos  7127  fliftfuns  7312  offval2  7694  ofmpteq  7697  mpocurryvald  8265  qliftfuns  8801  axcc2  10420  seqof2  14096  summolem2a  15766  zsum  15769  fsumcvg2  15778  fsumrlim  15863  cbvprod  15967  prodmolem2a  15988  zprod  15991  fprod  15995  pcmptdvds  16953  prdsdsval2  17536  gsumconstf  20004  gsummpt1n0  20034  gsum2d2  20043  dprd2d2  20115  gsumdixp  20399  psrass1lem  22062  coe1fzgsumdlem  22442  gsumply1eq  22448  evl1gsumdlem  22495  madugsum  22779  cnmpt1t  23801  cnmpt2k  23824  elmptrab  23963  flfcnp2  24143  prdsxmet  24505  fsumcn  25008  ovoliunlem3  25642  ovoliun  25643  ovoliun2  25644  voliun  25692  mbfpos  25789  mbfposb  25791  i1fposd  25845  itg2cnlem1  25899  isibl2  25904  cbvitg  25914  itgss3  25953  itgfsum  25965  itgabs  25973  itgcn  25983  limcmpt  26021  dvmptfsum  26113  lhop2  26153  dvfsumle  26159  dvfsumlem2  26165  itgsubstlem  26186  itgsubst  26187  itgulm2  26548  rlimcnp2  27107  gsummpt2co  33334  gsumpart  33349  esumsnf  34420  mbfposadd  38284  itgabsnc  38306  ftc1cnnclem  38308  ftc2nc  38319  zndvdchrrhm  42708  aks6d1c1  42851  evl1gprodd  42852  aks6d1c2  42865  idomnnzgmulnz  42868  deg1gprod  42875  sticksstones12a  42892  aks6d1c6lem5  42912  aks6d1c7lem2  42916  aks6d1c7lem3  42917  aks5lem4a  42925  mzpsubst  43449  rabdiophlem2  43499  aomclem8  43758  fsumcnf  45711  disjf1  45871  disjrnmpt2  45876  disjinfi  45880  fmptf  45924  cncfmptss  46273  mulc1cncfg  46275  expcnfg  46277  fprodcn  46286  fnlimabslt  46363  climmptf  46365  liminfvalxr  46467  liminfpnfuz  46500  xlimpnfxnegmnf2  46542  icccncfext  46571  cncficcgt0  46572  cncfiooicclem1  46577  fprodcncf  46584  dvmptmulf  46621  iblsplitf  46654  stoweidlem21  46705  stirlinglem4  46761  stirlinglem13  46770  stirlinglem15  46772  fourierd  46906  fourierclimd  46907  sge0iunmptlemre  47099  sge0iunmpt  47102  sge0ltfirpmpt2  47110  sge0isummpt2  47116  sge0xaddlem2  47118  sge0xadd  47119  meadjiun  47150  meaiunincf  47167  meaiuninc3  47169  omeiunle  47201  caratheodorylem2  47211  ovncvrrp  47248  vonioo  47366  smflim2  47490  smfsup  47498  smfinf  47502  smflimsup  47512  smfliminf  47515