Theorem cbvmpt 5253

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 2366. See cbvmptg 5254 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 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 2898	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2898	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvmpt.1	. 2 ⊢ Ⅎ𝑦𝐵
4		cbvmpt.2	. 2 ⊢ Ⅎ𝑥𝐶
5		cbvmpt.3	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
6	1, 2, 3, 4, 5	cbvmptf 5251	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1534  Ⅎwnfc 2878   ↦ cmpt 5225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-opab 5205  df-mpt 5226

This theorem is referenced by:  cbvmptvOLD  5256  dffn5f  6964  fvmpts  7002  fvmpt2i  7009  fvmptex  7013  fmptcof  7133  fmptcos  7134  fliftfuns  7316  offval2  7699  ofmpteq  7701  mpocurryvald  8269  qliftfuns  8814  axcc2  10452  seqof2  14049  summolem2a  15685  zsum  15688  fsumcvg2  15697  fsumrlim  15781  cbvprod  15883  prodmolem2a  15902  zprod  15905  fprod  15909  pcmptdvds  16854  prdsdsval2  17457  gsumconstf  19881  gsummpt1n0  19911  gsum2d2  19920  dprd2d2  19992  gsumdixp  20244  psrass1lemOLD  21861  psrass1lem  21864  coe1fzgsumdlem  22209  gsumply1eq  22215  evl1gsumdlem  22262  madugsum  22532  cnmpt1t  23556  cnmpt2k  23579  elmptrab  23718  flfcnp2  23898  prdsxmet  24262  fsumcn  24775  ovoliunlem3  25420  ovoliun  25421  ovoliun2  25422  voliun  25470  mbfpos  25567  mbfposb  25569  i1fposd  25624  itg2cnlem1  25678  isibl2  25683  cbvitg  25692  itgss3  25731  itgfsum  25743  itgabs  25751  itgcn  25761  limcmpt  25799  dvmptfsum  25894  lhop2  25935  dvfsumle  25941  dvfsumleOLD  25942  dvfsumlem2  25948  dvfsumlem2OLD  25949  itgsubstlem  25970  itgsubst  25971  itgulm2  26332  rlimcnp2  26885  gsummpt2co  32740  gsumpart  32747  esumsnf  33619  mbfposadd  37075  itgabsnc  37097  ftc1cnnclem  37099  ftc2nc  37110  aks6d1c1  41520  evl1gprodd  41521  aks6d1c2  41533  idomnnzgmulnz  41536  deg1gprod  41544  sticksstones12a  41561  mzpsubst  42090  rabdiophlem2  42144  aomclem8  42407  fsumcnf  44306  disjf1  44479  disjrnmpt2  44484  disjinfi  44488  fmptf  44537  cncfmptss  44898  mulc1cncfg  44900  expcnfg  44902  fprodcn  44911  fnlimabslt  44990  climmptf  44992  liminfvalxr  45094  liminfpnfuz  45127  xlimpnfxnegmnf2  45169  icccncfext  45198  cncficcgt0  45199  cncfiooicclem1  45204  fprodcncf  45211  dvmptmulf  45248  iblsplitf  45281  stoweidlem21  45332  stirlinglem4  45388  stirlinglem13  45397  stirlinglem15  45399  fourierd  45533  fourierclimd  45534  sge0iunmptlemre  45726  sge0iunmpt  45729  sge0ltfirpmpt2  45737  sge0isummpt2  45743  sge0xaddlem2  45745  sge0xadd  45746  meadjiun  45777  meaiunincf  45794  meaiuninc3  45796  omeiunle  45828  caratheodorylem2  45838  ovncvrrp  45875  vonioo  45993  smflim2  46117  smfsup  46125  smfinf  46129  smflimsup  46139  smfliminf  46142