Theorem cbvmpt 5167

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

Syntax hints:   → wi 4   = wceq 1537  Ⅎwnfc 2961   ↦ cmpt 5146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5129  df-mpt 5147

This theorem is referenced by:  cbvmptv  5169  dffn5f  6736  fvmpts  6771  fvmpt2i  6778  fvmptex  6782  fmptcof  6892  fmptcos  6893  fliftfuns  7067  offval2  7426  ofmpteq  7428  mpocurryvald  7936  qliftfuns  8384  axcc2  9859  seqof2  13429  summolem2a  15072  zsum  15075  fsumcvg2  15084  fsumrlim  15166  cbvprod  15269  prodmolem2a  15288  zprod  15291  fprod  15295  pcmptdvds  16230  prdsdsval2  16757  gsumconstf  19055  gsummpt1n0  19085  gsum2d2  19094  dprd2d2  19166  gsumdixp  19359  psrass1lem  20157  coe1fzgsumdlem  20469  gsumply1eq  20473  evl1gsumdlem  20519  madugsum  21252  cnmpt1t  22273  cnmpt2k  22296  elmptrab  22435  flfcnp2  22615  prdsxmet  22979  fsumcn  23478  ovoliunlem3  24105  ovoliun  24106  ovoliun2  24107  voliun  24155  mbfpos  24252  mbfposb  24254  i1fposd  24308  itg2cnlem1  24362  isibl2  24367  cbvitg  24376  itgss3  24415  itgfsum  24427  itgabs  24435  itgcn  24443  limcmpt  24481  dvmptfsum  24572  lhop2  24612  dvfsumle  24618  dvfsumlem2  24624  itgsubstlem  24645  itgsubst  24646  itgulm2  24997  rlimcnp2  25544  gsummpt2co  30686  esumsnf  31323  mbfposadd  34954  itgabsnc  34976  ftc1cnnclem  34980  ftc2nc  34991  mzpsubst  39394  rabdiophlem2  39448  aomclem8  39710  fsumcnf  41327  disjf1  41492  disjrnmpt2  41498  disjinfi  41503  fmptf  41558  cncfmptss  41917  mulc1cncfg  41919  expcnfg  41921  fprodcn  41930  fnlimabslt  42009  climmptf  42011  liminfvalxr  42113  liminfpnfuz  42146  xlimpnfxnegmnf2  42188  icccncfext  42219  cncficcgt0  42220  cncfiooicclem1  42225  fprodcncf  42233  dvmptmulf  42271  iblsplitf  42304  stoweidlem21  42355  stirlinglem4  42411  stirlinglem13  42420  stirlinglem15  42422  fourierd  42556  fourierclimd  42557  sge0iunmptlemre  42746  sge0iunmpt  42749  sge0ltfirpmpt2  42757  sge0isummpt2  42763  sge0xaddlem2  42765  sge0xadd  42766  meadjiun  42797  meaiunincf  42814  meaiuninc3  42816  omeiunle  42848  caratheodorylem2  42858  ovncvrrp  42895  vonioo  43013  smflim2  43129  smfsup  43137  smfinf  43141  smflimsup  43151  smfliminf  43154