Theorem cbvmpt 5210

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Ⅎwnfc 2911   ↦ cmpt 5189

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5171  df-mpt 5190

This theorem is used by:  dffn5f  6979  fvmpts  7020  fvmpt2i  7027  fvmptex  7031  fmptcof  7155  fmptcos  7156  fliftfuns  7345  offval2  7737  ofmpteq  7740  mpocurryvald  8315  qliftfuns  8853  axcc2  10542  seqof2  14230  summolem2a  15910  zsum  15913  fsumcvg2  15922  fsumrlim  16007  cbvprod  16111  prodmolem2a  16130  zprod  16133  fprod  16137  pcmptdvds  17101  prdsdsval2  17684  gsumconstf  20179  gsummpt1n0  20209  gsum2d2  20218  dprd2d2  20290  gsumdixp  20578  psrass1lem  22271  coe1fzgsumdlem  22651  gsumply1eq  22657  evl1gsumdlem  22704  madugsum  22988  cnmpt1t  24014  cnmpt2k  24037  elmptrab  24176  flfcnp2  24356  prdsxmet  24718  fsumcn  25221  ovoliunlem3  25855  ovoliun  25856  ovoliun2  25857  voliun  25905  mbfpos  26002  mbfposb  26004  i1fposd  26058  itg2cnlem1  26112  isibl2  26117  cbvitg  26126  itgss3  26165  itgfsum  26177  itgabs  26185  itgcn  26195  limcmpt  26233  dvmptfsum  26325  lhop2  26365  dvfsumle  26371  dvfsumlem2  26377  itgsubstlem  26398  itgsubst  26399  itgulm2  26766  rlimcnp2  27324  gsummpt2co  33679  gsumpart  33694  esumsnf  34766  mbfposadd  38777  itgabsnc  38799  ftc1cnnclem  38801  ftc2nc  38812  zndvdchrrhm  43215  aks6d1c1  43358  evl1gprodd  43359  aks6d1c2  43372  idomnnzgmulnz  43375  deg1gprod  43382  sticksstones12a  43399  aks6d1c6lem5  43419  aks6d1c7lem2  43423  aks6d1c7lem3  43424  aks5lem4a  43432  mzpsubst  43952  rabdiophlem2  44002  aomclem8  44256  fsumcnf  46243  disjf1  46403  disjrnmpt2  46408  disjinfi  46412  fmptf  46456  cncfmptss  46804  mulc1cncfg  46806  expcnfg  46808  fprodcn  46817  fnlimabslt  46894  climmptf  46896  liminfvalxr  46998  liminfpnfuz  47031  xlimpnfxnegmnf2  47073  icccncfext  47102  cncficcgt0  47103  cncfiooicclem1  47108  fprodcncf  47115  dvmptmulf  47152  iblsplitf  47185  stoweidlem21  47236  stirlinglem4  47292  stirlinglem13  47301  stirlinglem15  47303  fourierd  47437  fourierclimd  47438  sge0iunmptlemre  47630  sge0iunmpt  47633  sge0ltfirpmpt2  47641  sge0isummpt2  47647  sge0xaddlem2  47649  sge0xadd  47650  meadjiun  47681  meaiunincf  47698  meaiuninc3  47700  omeiunle  47732  caratheodorylem2  47742  ovncvrrp  47779  vonioo  47897  smflim2  48021  smfsup  48029  smfinf  48033  smflimsup  48043  smfliminf  48046