MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvmptv Structured version   Unicode version

Theorem cbvmptv 4528
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
Hypothesis
Ref Expression
cbvmptv.1  |-  ( x  =  y  ->  B  =  C )
Assertion
Ref Expression
cbvmptv  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Distinct variable groups:    x, A    y, A    y, B    x, C
Allowed substitution hints:    B( x)    C( y)

Proof of Theorem cbvmptv
StepHypRef Expression
1 nfcv 2605 . 2  |-  F/_ y B
2 nfcv 2605 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4527 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    |-> cmpt 4495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-opab 4496  df-mpt 4497
This theorem is referenced by:  fnmptfvd  5975  onnseq  7017  rdgsucmpt2  7098  frsucmpt2  7107  resixpfo  7509  pw2f1olem  7623  xpmapen  7687  dffi3  7893  ordtypecbv  7945  inf3lema  8044  cantnflem1  8111  cantnflem1OLD  8134  cnfcomlem  8146  cnfcomlemOLD  8154  infxpenc2  8402  infxpenc2OLD  8406  fseqenlem1  8408  dfac8a  8414  dfac12r  8529  r1om  8627  fictb  8628  cfsmo  8654  coftr  8656  fin23lem38  8732  compsscnv  8754  isf34lem1  8755  compss  8759  fin1a2lem1  8783  fin1a2lem3  8785  fin1a2lem13  8795  itunisuc  8802  hsmex  8815  domtriom  8826  axdc2  8832  zorn2g  8886  ttukey2g  8899  axdc  8904  konigth  8947  pwcfsdom  8961  canthp1  9035  wunex2  9119  wuncval2  9128  negiso  10526  reexALT  11224  caurcvg2  13481  caucvg  13482  summo  13520  zsum  13521  fsum  13523  ackbijnn  13621  prodmo  13724  zprod  13725  fprod  13729  iprodmul  13777  rpnnen  13941  phimullem  14290  eulerth  14294  iserodd  14340  prmreclem5  14419  prmrec  14421  vdwlem7  14486  vdwlem9  14488  vdwlem10  14489  ramub1  14527  ramcl  14528  yonedalem4c  15524  yonedalem3b  15526  gsumwspan  15992  grplactcnv  16116  galactghm  16406  symgfixfo  16442  pmtrdifwrdel  16488  pmtrdifwrdel2  16489  odf1o2  16571  sylow1lem2  16597  sylow1  16601  sylow2b  16621  sylow3lem1  16625  sylow3lem5  16629  sylow3  16631  efgtf  16718  efgsval  16727  ghmcyg  16876  cycsubgcyg  16881  ablfaclem3  17116  ablfac2  17118  srgbinomlem4  17172  fidomndrnglem  17933  mplmonmul  18104  evlslem2  18158  isphld  18666  frlmphl  18789  mat1ric  18966  mdetralt  19087  smadiadetlem3  19147  pmatcollpw3lem  19261  mp2pm2mplem5  19288  mp2pm2mp  19289  pm2mpmhmlem2  19297  cpmidpmat  19351  cpmadugsumlemF  19354  cpmadugsumfi  19355  cpmadumatpoly  19361  chcoeffeqlem  19363  cayleyhamilton0  19367  cayleyhamilton  19368  cayleyhamiltonALT  19369  cayleyhamilton1  19370  ordtbaslem  19666  ordtbas2  19669  lly1stc  19974  ptpjopn  20090  xkohmeo  20293  fbasrn  20362  elfm  20425  tmdmulg  20568  tmdgsum  20571  qustgpopn  20595  tsmsfbas  20603  tsmsf1o  20624  ustuqtoplem  20719  utopsnneip  20728  fmucnd  20772  ucnextcn  20784  met1stc  21001  prdsxmslem2  21009  metusttoOLD  21037  metustto  21038  metustexhalfOLD  21043  metustexhalf  21044  metuustOLD  21051  metuust  21052  cfilucfil2OLD  21053  cfilucfil2  21054  metuelOLD  21057  metuel  21058  metuel2  21059  metutopOLD  21062  psmetutop  21063  restmetu  21067  metucnOLD  21068  metucn  21069  xrge0tsms  21316  metdsge  21330  expcn  21353  pi1xfrcnv  21534  minveclem3b  21820  minveclem5  21825  minvec  21828  ovollb2  21877  ovolshftlem2  21898  ovolscalem2  21902  ovolicc  21911  ioombl1  21949  uniioombllem6  21974  volsup2  21991  vitali  21999  mbfi1fseq  22105  mbfmullem  22109  itg2seq  22126  itg2i1fseq  22139  itg2addlem  22142  itg2cnlem1  22145  itg2cn  22147  dvfsumrlimge0  22408  plyadd  22591  plymul  22592  coeeu  22599  coeid  22612  dvply2g  22657  plydivex  22669  elqaalem2  22692  elqaa  22694  taylthlem1  22744  taylth  22746  pserval  22781  radcnvlem2  22785  radcnvlt2  22790  dvradcnv  22792  pserulm  22793  psercn  22797  pserdvlem2  22799  pserdv  22800  efgh  22904  eff1olem  22911  circgrp  22915  circsubm  22916  logno1  22993  emcl  23308  harmonicbnd  23309  harmonicbnd2  23310  basel  23339  musum  23443  dchr1  23508  dchrptlem2  23516  dchrpt  23518  lgsqrlem4  23595  lgseisenlem3  23602  2sqlem1  23614  dchrmusumlema  23654  dchrmusum2  23655  dchrvmasumlema  23661  dchrvmasumiflem1  23662  dchrisum0ff  23668  dchrisum0lema  23675  dchrisum0lem1b  23676  dchrisum0lem2a  23678  wlknwwlknvbij  24716  clwlksizeeq  24828  rusgranumwlkg  24934  frgrancvvdeqlemB  25014  frgrancvvdeqlemC  25015  numclwwlk7  25090  ubthlem3  25764  minveco  25776  htth  25811  xrge0tsmsd  27752  xrge0mulc1cn  27900  xrge0tmdOLD  27904  xrge0tmd  27905  gsumesum  28044  esumlub  28045  esumpcvgval  28061  esumcvg  28069  esumcvg2  28070  eulerpartlems  28276  eulerpart  28298  fibp1  28317  rrvadd  28368  ballotlemfval  28405  ballotlemi  28416  ballotlemsval  28424  ballotlemsv  28425  ballotlemsf1o  28429  ballotlemrval  28433  ballotlemrinv  28449  signsply0  28485  derangfmla  28611  erdsze  28623  pconpi1  28659  cvmscbv  28680  cvmsss2  28696  cvmliftlem15  28720  cvmlift2  28738  cvmlift3  28750  elmrsubrn  28857  relexpsucr  29030  iprodefisum  29099  trpredtr  29288  trpredmintr  29289  bpolyval  29786  fin2so  30015  ftc1anclem5  30069  ftc1anclem6  30070  sdclem2  30210  prdstotbnd  30265  prdsbnd2  30266  heiborlem10  30291  mzpclval  30632  mzpcompact2lem  30659  rmxyval  30826  dnnumch1  30965  aomclem3  30977  aomclem8  30982  dfac21  30987  pwfi2f1o  31019  radcnvrat  31171  expgrowthi  31214  expgrowth  31216  fmuldfeqlem1  31504  sumnnodd  31544  dvsinax  31612  fperdvper  31619  dvcosax  31627  ioodvbdlimc1lem1  31632  ioodvbdlimc1  31634  ioodvbdlimc2  31636  itgsin0pilem1  31638  itgiccshift  31669  stoweidlem2  31673  stoweidlem17  31688  stoweidlem32  31703  stoweidlem34  31705  stoweidlem43  31714  stirlinglem2  31746  stirlinglem3  31747  stirlinglem8  31752  dirkerval  31762  dirkerval2  31765  dirkeritg  31773  dirkercncflem3  31776  dirkercncf  31778  fourierdlem14  31792  fourierdlem18  31796  fourierdlem53  31831  fourierdlem62  31840  fourierdlem71  31849  fourierdlem74  31852  fourierdlem75  31853  fourierdlem76  31854  fourierdlem80  31858  fourierdlem81  31859  fourierdlem84  31862  fourierdlem88  31866  fourierdlem92  31870  fourierdlem93  31871  fourierdlem94  31872  fourierdlem95  31873  fourierdlem96  31874  fourierdlem97  31875  fourierdlem98  31876  fourierdlem99  31877  fourierdlem101  31879  fourierdlem103  31881  fourierdlem104  31882  fourierdlem105  31883  fourierdlem106  31884  fourierdlem107  31885  fourierdlem108  31886  fourierdlem110  31888  fourierdlem111  31889  fourierdlem112  31890  fourierdlem113  31891  fourierdlem115  31893  fouriersw  31903  usgedgvadf1  32253  usgedgvadf1ALT  32256  funcrngcsetcALT  32547  rmsupp0  32696  domnmsuppn0  32697  rmsuppss  32698  suppmptcfin  32707  ply1mulgsum  32725  lcoc0  32758  linc1  32761  lcoel0  32764  lcoss  32772  el0ldep  32802  lincresunit3  32817  isldepslvec2  32821  lshpkrcl  34581  tendoplcbv  36241  tendo0cbv  36252  tendoicbv  36259  lcfl7N  36968  lcf1o  37018  hdmap1cbv  37270
  Copyright terms: Public domain W3C validator