Theorem cbvmpt 5277

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

Syntax hints:   → wi 4   = wceq 1537  Ⅎwnfc 2893   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-opab 5229  df-mpt 5250

This theorem is referenced by:  cbvmptvOLD  5280  dffn5f  6993  fvmpts  7032  fvmpt2i  7039  fvmptex  7043  fmptcof  7164  fmptcos  7165  fliftfuns  7350  offval2  7734  ofmpteq  7736  mpocurryvald  8311  qliftfuns  8862  axcc2  10506  seqof2  14111  summolem2a  15763  zsum  15766  fsumcvg2  15775  fsumrlim  15859  cbvprod  15961  prodmolem2a  15982  zprod  15985  fprod  15989  pcmptdvds  16941  prdsdsval2  17544  gsumconstf  19977  gsummpt1n0  20007  gsum2d2  20016  dprd2d2  20088  gsumdixp  20342  psrass1lem  21975  coe1fzgsumdlem  22328  gsumply1eq  22334  evl1gsumdlem  22381  madugsum  22670  cnmpt1t  23694  cnmpt2k  23717  elmptrab  23856  flfcnp2  24036  prdsxmet  24400  fsumcn  24913  ovoliunlem3  25558  ovoliun  25559  ovoliun2  25560  voliun  25608  mbfpos  25705  mbfposb  25707  i1fposd  25762  itg2cnlem1  25816  isibl2  25821  cbvitg  25831  itgss3  25870  itgfsum  25882  itgabs  25890  itgcn  25900  limcmpt  25938  dvmptfsum  26033  lhop2  26074  dvfsumle  26080  dvfsumleOLD  26081  dvfsumlem2  26087  dvfsumlem2OLD  26088  itgsubstlem  26109  itgsubst  26110  itgulm2  26470  rlimcnp2  27027  gsummpt2co  33031  gsumpart  33038  esumsnf  34028  mbfposadd  37627  itgabsnc  37649  ftc1cnnclem  37651  ftc2nc  37662  zndvdchrrhm  41927  aks6d1c1  42073  evl1gprodd  42074  aks6d1c2  42087  idomnnzgmulnz  42090  deg1gprod  42097  sticksstones12a  42114  aks6d1c6lem5  42134  aks6d1c7lem2  42138  aks6d1c7lem3  42139  aks5lem4a  42147  mzpsubst  42704  rabdiophlem2  42758  aomclem8  43018  fsumcnf  44921  disjf1  45090  disjrnmpt2  45095  disjinfi  45099  fmptf  45147  cncfmptss  45508  mulc1cncfg  45510  expcnfg  45512  fprodcn  45521  fnlimabslt  45600  climmptf  45602  liminfvalxr  45704  liminfpnfuz  45737  xlimpnfxnegmnf2  45779  icccncfext  45808  cncficcgt0  45809  cncfiooicclem1  45814  fprodcncf  45821  dvmptmulf  45858  iblsplitf  45891  stoweidlem21  45942  stirlinglem4  45998  stirlinglem13  46007  stirlinglem15  46009  fourierd  46143  fourierclimd  46144  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0ltfirpmpt2  46347  sge0isummpt2  46353  sge0xaddlem2  46355  sge0xadd  46356  meadjiun  46387  meaiunincf  46404  meaiuninc3  46406  omeiunle  46438  caratheodorylem2  46448  ovncvrrp  46485  vonioo  46603  smflim2  46727  smfsup  46735  smfinf  46739  smflimsup  46749  smfliminf  46752