MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvmpt Structured version   Visualization version   GIF version

Theorem cbvmpt 5217
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 2371. See cbvmptg 5218 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
StepHypRef Expression
1 nfcv 2904 . 2 𝑥𝐴
2 nfcv 2904 . 2 𝑦𝐴
3 cbvmpt.1 . 2 𝑦𝐵
4 cbvmpt.2 . 2 𝑥𝐶
5 cbvmpt.3 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
61, 2, 3, 4, 5cbvmptf 5215 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wnfc 2884  cmpt 5189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5169  df-mpt 5190
This theorem is referenced by:  cbvmptvOLD  5220  dffn5f  6914  fvmpts  6952  fvmpt2i  6959  fvmptex  6963  fmptcof  7077  fmptcos  7078  fliftfuns  7260  offval2  7638  ofmpteq  7640  mpocurryvald  8202  qliftfuns  8746  axcc2  10378  seqof2  13972  summolem2a  15605  zsum  15608  fsumcvg2  15617  fsumrlim  15701  cbvprod  15803  prodmolem2a  15822  zprod  15825  fprod  15829  pcmptdvds  16771  prdsdsval2  17371  gsumconstf  19717  gsummpt1n0  19747  gsum2d2  19756  dprd2d2  19828  gsumdixp  20038  psrass1lemOLD  21358  psrass1lem  21361  coe1fzgsumdlem  21688  gsumply1eq  21692  evl1gsumdlem  21738  madugsum  22008  cnmpt1t  23032  cnmpt2k  23055  elmptrab  23194  flfcnp2  23374  prdsxmet  23738  fsumcn  24249  ovoliunlem3  24884  ovoliun  24885  ovoliun2  24886  voliun  24934  mbfpos  25031  mbfposb  25033  i1fposd  25088  itg2cnlem1  25142  isibl2  25147  cbvitg  25156  itgss3  25195  itgfsum  25207  itgabs  25215  itgcn  25225  limcmpt  25263  dvmptfsum  25355  lhop2  25395  dvfsumle  25401  dvfsumlem2  25407  itgsubstlem  25428  itgsubst  25429  itgulm2  25784  rlimcnp2  26332  gsummpt2co  31939  gsumpart  31946  esumsnf  32720  mbfposadd  36171  itgabsnc  36193  ftc1cnnclem  36195  ftc2nc  36206  sticksstones12a  40611  mzpsubst  41114  rabdiophlem2  41168  aomclem8  41431  fsumcnf  43314  disjf1  43489  disjrnmpt2  43495  disjinfi  43500  fmptf  43552  cncfmptss  43914  mulc1cncfg  43916  expcnfg  43918  fprodcn  43927  fnlimabslt  44006  climmptf  44008  liminfvalxr  44110  liminfpnfuz  44143  xlimpnfxnegmnf2  44185  icccncfext  44214  cncficcgt0  44215  cncfiooicclem1  44220  fprodcncf  44227  dvmptmulf  44264  iblsplitf  44297  stoweidlem21  44348  stirlinglem4  44404  stirlinglem13  44413  stirlinglem15  44415  fourierd  44549  fourierclimd  44550  sge0iunmptlemre  44742  sge0iunmpt  44745  sge0ltfirpmpt2  44753  sge0isummpt2  44759  sge0xaddlem2  44761  sge0xadd  44762  meadjiun  44793  meaiunincf  44810  meaiuninc3  44812  omeiunle  44844  caratheodorylem2  44854  ovncvrrp  44891  vonioo  45009  smflim2  45133  smfsup  45141  smfinf  45145  smflimsup  45155  smfliminf  45158
  Copyright terms: Public domain W3C validator