Theorem cbvmpt 5160

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 2386. See cbvmptg 5161 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 5158	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1533  Ⅎwnfc 2961   ↦ cmpt 5139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5122  df-mpt 5140

This theorem is referenced by:  cbvmptv  5162  dffn5f  6731  fvmpts  6766  fvmpt2i  6773  fvmptex  6777  fmptcof  6887  fmptcos  6888  fliftfuns  7061  offval2  7420  ofmpteq  7422  mpocurryvald  7930  qliftfuns  8378  axcc2  9853  seqof2  13422  summolem2a  15066  zsum  15069  fsumcvg2  15078  fsumrlim  15160  cbvprod  15263  prodmolem2a  15282  zprod  15285  fprod  15289  pcmptdvds  16224  prdsdsval2  16751  gsumconstf  19049  gsummpt1n0  19079  gsum2d2  19088  dprd2d2  19160  gsumdixp  19353  psrass1lem  20151  coe1fzgsumdlem  20463  gsumply1eq  20467  evl1gsumdlem  20513  madugsum  21246  cnmpt1t  22267  cnmpt2k  22290  elmptrab  22429  flfcnp2  22609  prdsxmet  22973  fsumcn  23472  ovoliunlem3  24099  ovoliun  24100  ovoliun2  24101  voliun  24149  mbfpos  24246  mbfposb  24248  i1fposd  24302  itg2cnlem1  24356  isibl2  24361  cbvitg  24370  itgss3  24409  itgfsum  24421  itgabs  24429  itgcn  24437  limcmpt  24475  dvmptfsum  24566  lhop2  24606  dvfsumle  24612  dvfsumlem2  24618  itgsubstlem  24639  itgsubst  24640  itgulm2  24991  rlimcnp2  25538  gsummpt2co  30681  esumsnf  31318  mbfposadd  34933  itgabsnc  34955  ftc1cnnclem  34959  ftc2nc  34970  mzpsubst  39338  rabdiophlem2  39392  aomclem8  39654  fsumcnf  41271  disjf1  41435  disjrnmpt2  41441  disjinfi  41446  fmptf  41501  cncfmptss  41860  mulc1cncfg  41862  expcnfg  41864  fprodcn  41873  fnlimabslt  41952  climmptf  41954  liminfvalxr  42056  liminfpnfuz  42089  xlimpnfxnegmnf2  42131  icccncfext  42162  cncficcgt0  42163  cncfiooicclem1  42168  fprodcncf  42176  dvmptmulf  42214  iblsplitf  42247  stoweidlem21  42299  stirlinglem4  42355  stirlinglem13  42364  stirlinglem15  42366  fourierd  42500  fourierclimd  42501  sge0iunmptlemre  42690  sge0iunmpt  42693  sge0ltfirpmpt2  42701  sge0isummpt2  42707  sge0xaddlem2  42709  sge0xadd  42710  meadjiun  42741  meaiunincf  42758  meaiuninc3  42760  omeiunle  42792  caratheodorylem2  42802  ovncvrrp  42839  vonioo  42957  smflim2  43073  smfsup  43081  smfinf  43085  smflimsup  43095  smfliminf  43098