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

Theorem cbvmptv 4371
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 2569 . 2  |-  F/_ y B
2 nfcv 2569 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4370 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. cmpt 4338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-opab 4339  df-mpt 4340
This theorem is referenced by:  fnmptfvd  5794  onnseq  6791  rdgsucmpt2  6872  frsucmpt2  6881  resixpfo  7289  pw2f1olem  7403  xpmapen  7467  dffi3  7669  ordtypecbv  7719  inf3lema  7818  cantnflem1  7885  cantnflem1OLD  7908  cnfcomlem  7920  cnfcomlemOLD  7928  infxpenc2  8176  infxpenc2OLD  8180  fseqenlem1  8182  dfac8a  8188  dfac12r  8303  r1om  8401  fictb  8402  cfsmo  8428  coftr  8430  fin23lem38  8506  compsscnv  8528  isf34lem1  8529  compss  8533  fin1a2lem1  8557  fin1a2lem3  8559  fin1a2lem13  8569  itunisuc  8576  hsmex  8589  domtriom  8600  axdc2  8606  zorn2g  8660  ttukey2g  8673  axdc  8678  konigth  8721  pwcfsdom  8735  canthp1  8808  wunex2  8892  wuncval2  8901  negiso  10293  reexALT  10972  caurcvg2  13138  caucvg  13139  summo  13177  zsum  13178  fsum  13180  ackbijnn  13273  rpnnen  13491  phimullem  13836  eulerth  13840  iserodd  13884  prmreclem5  13963  prmrec  13965  vdwlem7  14030  vdwlem9  14032  vdwlem10  14033  ramub1  14071  ramcl  14072  yonedalem4c  15069  yonedalem3b  15071  gsumwspan  15503  grplactcnv  15603  galactghm  15887  symgfixfo  15924  pmtrdifwrdel  15970  pmtrdifwrdel2  15971  odf1o2  16051  sylow1lem2  16077  sylow1  16081  sylow2b  16101  sylow3lem1  16105  sylow3lem5  16109  sylow3  16111  efgtf  16198  efgsval  16207  ghmcyg  16351  cycsubgcyg  16356  ablfaclem3  16561  ablfac2  16563  fidomndrnglem  17299  mplmonmul  17476  evlslem2  17524  isphld  17924  frlmphl  18047  mdetralt  18255  smadiadetlem3  18315  ordtbaslem  18633  ordtbas2  18636  lly1stc  18941  ptpjopn  19026  xkohmeo  19229  fbasrn  19298  elfm  19361  tmdmulg  19504  tmdgsum  19507  divstgpopn  19531  tsmsfbas  19539  tsmsf1o  19560  ustuqtoplem  19655  utopsnneip  19664  fmucnd  19708  ucnextcn  19720  met1stc  19937  prdsxmslem2  19945  metusttoOLD  19973  metustto  19974  metustexhalfOLD  19979  metustexhalf  19980  metuustOLD  19987  metuust  19988  cfilucfil2OLD  19989  cfilucfil2  19990  metuelOLD  19993  metuel  19994  metuel2  19995  metutopOLD  19998  psmetutop  19999  restmetu  20003  metucnOLD  20004  metucn  20005  xrge0tsms  20252  metdsge  20266  expcn  20289  pi1xfrcnv  20470  minveclem3b  20756  minveclem5  20761  minvec  20764  ovollb2  20813  ovolshftlem2  20834  ovolscalem2  20838  ovolicc  20847  ioombl1  20884  uniioombllem6  20909  volsup2  20926  vitali  20934  mbfi1fseq  21040  mbfmullem  21044  itg2seq  21061  itg2i1fseq  21074  itg2addlem  21077  itg2cnlem1  21080  itg2cn  21082  dvfsumrlimge0  21343  plyadd  21569  plymul  21570  coeeu  21577  coeid  21590  dvply2g  21635  plydivex  21647  elqaalem2  21670  elqaa  21672  taylthlem1  21722  taylth  21724  pserval  21759  radcnvlem2  21763  radcnvlt2  21768  dvradcnv  21770  pserulm  21771  psercn  21775  pserdvlem2  21777  pserdv  21778  eff1olem  21888  logno1  21965  emcl  22280  harmonicbnd  22281  harmonicbnd2  22282  basel  22311  musum  22415  dchr1  22480  dchrptlem2  22488  dchrpt  22490  lgsqrlem4  22567  lgseisenlem3  22574  2sqlem1  22586  dchrmusumlema  22626  dchrmusum2  22627  dchrvmasumlema  22633  dchrvmasumiflem1  22634  dchrisum0ff  22640  dchrisum0lema  22647  dchrisum0lem1b  22648  dchrisum0lem2a  22650  ubthlem3  24095  minveco  24107  htth  24142  xrge0tsmsd  26105  xrge0mulc1cn  26224  xrge0tmdOLD  26228  gsumesum  26363  esumlub  26364  esumpcvgval  26380  esumcvg  26388  esumcvg2  26389  eulerpartlems  26590  eulerpart  26612  fibp1  26631  rrvadd  26682  ballotlemfval  26719  ballotlemi  26730  ballotlemsval  26738  ballotlemsv  26739  ballotlemsf1o  26743  ballotlemrval  26747  ballotlemrinv  26763  signsply0  26799  derangfmla  26925  erdsze  26937  pconpi1  26973  cvmscbv  26994  cvmsss2  27010  cvmliftlem15  27034  cvmlift2  27052  cvmlift3  27064  relexpsucr  27178  prodmo  27295  zprod  27296  fprod  27300  iprodmul  27349  iprodefisum  27351  trpredtr  27540  trpredmintr  27541  bpolyval  28038  fin2so  28257  ftc1anclem5  28312  ftc1anclem6  28313  sdclem2  28479  prdstotbnd  28534  prdsbnd2  28535  heiborlem10  28560  mzpclval  28903  mzpcompact2lem  28930  rmxyval  29098  dnnumch1  29239  aomclem3  29251  aomclem8  29256  dfac21  29261  pwfi2f1o  29293  expgrowthi  29449  expgrowth  29451  fmuldfeqlem1  29605  itgsin0pilem1  29633  stoweidlem2  29640  stoweidlem17  29655  stoweidlem32  29670  stoweidlem34  29672  stoweidlem43  29681  stirlinglem2  29713  stirlinglem3  29714  stirlinglem8  29719  wlknwwlknvbij  30215  clwlksizeeq  30368  rusgranumwlkg  30419  frgrancvvdeqlemB  30474  frgrancvvdeqlemC  30475  numclwwlk7  30550  rmsupp0  30609  domnmsuppn0  30610  rmsuppss  30611  suppmptcfin  30620  lcoc0  30662  linc1  30665  lcoel0  30668  lcoss  30676  el0ldep  30706  lincresunit3  30721  isldepslvec2  30725  lshpkrcl  32331  tendoplcbv  33989  tendo0cbv  34000  tendoicbv  34007  lcfl7N  34716  lcf1o  34766  hdmap1cbv  35018
  Copyright terms: Public domain W3C validator