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

Theorem cbvmptv 4404
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 2589 . 2  |-  F/_ y B
2 nfcv 2589 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4403 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. cmpt 4371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-opab 4372  df-mpt 4373
This theorem is referenced by:  fnmptfvd  5827  onnseq  6826  rdgsucmpt2  6907  frsucmpt2  6916  resixpfo  7322  pw2f1olem  7436  xpmapen  7500  dffi3  7702  ordtypecbv  7752  inf3lema  7851  cantnflem1  7918  cantnflem1OLD  7941  cnfcomlem  7953  cnfcomlemOLD  7961  infxpenc2  8209  infxpenc2OLD  8213  fseqenlem1  8215  dfac8a  8221  dfac12r  8336  r1om  8434  fictb  8435  cfsmo  8461  coftr  8463  fin23lem38  8539  compsscnv  8561  isf34lem1  8562  compss  8566  fin1a2lem1  8590  fin1a2lem3  8592  fin1a2lem13  8602  itunisuc  8609  hsmex  8622  domtriom  8633  axdc2  8639  zorn2g  8693  ttukey2g  8706  axdc  8711  konigth  8754  pwcfsdom  8768  canthp1  8842  wunex2  8926  wuncval2  8935  negiso  10327  reexALT  11006  caurcvg2  13176  caucvg  13177  summo  13215  zsum  13216  fsum  13218  ackbijnn  13312  rpnnen  13530  phimullem  13875  eulerth  13879  iserodd  13923  prmreclem5  14002  prmrec  14004  vdwlem7  14069  vdwlem9  14071  vdwlem10  14072  ramub1  14110  ramcl  14111  yonedalem4c  15108  yonedalem3b  15110  gsumwspan  15545  grplactcnv  15645  galactghm  15929  symgfixfo  15966  pmtrdifwrdel  16012  pmtrdifwrdel2  16013  odf1o2  16093  sylow1lem2  16119  sylow1  16123  sylow2b  16143  sylow3lem1  16147  sylow3lem5  16151  sylow3  16153  efgtf  16240  efgsval  16249  ghmcyg  16393  cycsubgcyg  16398  ablfaclem3  16610  ablfac2  16612  srgbinomlem4  16663  fidomndrnglem  17400  mplmonmul  17565  evlslem2  17619  isphld  18105  frlmphl  18228  mdetralt  18436  smadiadetlem3  18496  ordtbaslem  18814  ordtbas2  18817  lly1stc  19122  ptpjopn  19207  xkohmeo  19410  fbasrn  19479  elfm  19542  tmdmulg  19685  tmdgsum  19688  divstgpopn  19712  tsmsfbas  19720  tsmsf1o  19741  ustuqtoplem  19836  utopsnneip  19845  fmucnd  19889  ucnextcn  19901  met1stc  20118  prdsxmslem2  20126  metusttoOLD  20154  metustto  20155  metustexhalfOLD  20160  metustexhalf  20161  metuustOLD  20168  metuust  20169  cfilucfil2OLD  20170  cfilucfil2  20171  metuelOLD  20174  metuel  20175  metuel2  20176  metutopOLD  20179  psmetutop  20180  restmetu  20184  metucnOLD  20185  metucn  20186  xrge0tsms  20433  metdsge  20447  expcn  20470  pi1xfrcnv  20651  minveclem3b  20937  minveclem5  20942  minvec  20945  ovollb2  20994  ovolshftlem2  21015  ovolscalem2  21019  ovolicc  21028  ioombl1  21065  uniioombllem6  21090  volsup2  21107  vitali  21115  mbfi1fseq  21221  mbfmullem  21225  itg2seq  21242  itg2i1fseq  21255  itg2addlem  21258  itg2cnlem1  21261  itg2cn  21263  dvfsumrlimge0  21524  plyadd  21707  plymul  21708  coeeu  21715  coeid  21728  dvply2g  21773  plydivex  21785  elqaalem2  21808  elqaa  21810  taylthlem1  21860  taylth  21862  pserval  21897  radcnvlem2  21901  radcnvlt2  21906  dvradcnv  21908  pserulm  21909  psercn  21913  pserdvlem2  21915  pserdv  21916  eff1olem  22026  logno1  22103  emcl  22418  harmonicbnd  22419  harmonicbnd2  22420  basel  22449  musum  22553  dchr1  22618  dchrptlem2  22626  dchrpt  22628  lgsqrlem4  22705  lgseisenlem3  22712  2sqlem1  22724  dchrmusumlema  22764  dchrmusum2  22765  dchrvmasumlema  22771  dchrvmasumiflem1  22772  dchrisum0ff  22778  dchrisum0lema  22785  dchrisum0lem1b  22786  dchrisum0lem2a  22788  ubthlem3  24295  minveco  24307  htth  24342  xrge0tsmsd  26275  xrge0mulc1cn  26393  xrge0tmdOLD  26397  gsumesum  26532  esumlub  26533  esumpcvgval  26549  esumcvg  26557  esumcvg2  26558  eulerpartlems  26765  eulerpart  26787  fibp1  26806  rrvadd  26857  ballotlemfval  26894  ballotlemi  26905  ballotlemsval  26913  ballotlemsv  26914  ballotlemsf1o  26918  ballotlemrval  26922  ballotlemrinv  26938  signsply0  26974  derangfmla  27100  erdsze  27112  pconpi1  27148  cvmscbv  27169  cvmsss2  27185  cvmliftlem15  27209  cvmlift2  27227  cvmlift3  27239  relexpsucr  27354  prodmo  27471  zprod  27472  fprod  27476  iprodmul  27525  iprodefisum  27527  trpredtr  27716  trpredmintr  27717  bpolyval  28214  fin2so  28442  ftc1anclem5  28497  ftc1anclem6  28498  sdclem2  28664  prdstotbnd  28719  prdsbnd2  28720  heiborlem10  28745  mzpclval  29087  mzpcompact2lem  29114  rmxyval  29282  dnnumch1  29423  aomclem3  29435  aomclem8  29440  dfac21  29445  pwfi2f1o  29477  expgrowthi  29633  expgrowth  29635  fmuldfeqlem1  29789  itgsin0pilem1  29816  stoweidlem2  29823  stoweidlem17  29838  stoweidlem32  29853  stoweidlem34  29855  stoweidlem43  29864  stirlinglem2  29896  stirlinglem3  29897  stirlinglem8  29902  wlknwwlknvbij  30398  clwlksizeeq  30551  rusgranumwlkg  30602  frgrancvvdeqlemB  30657  frgrancvvdeqlemC  30658  numclwwlk7  30733  rmsupp0  30811  domnmsuppn0  30812  rmsuppss  30813  suppmptcfin  30823  ply1mulgsum  30881  lcoc0  30953  linc1  30956  lcoel0  30959  lcoss  30967  el0ldep  30997  lincresunit3  31012  isldepslvec2  31016  mp2pm2mplem5  31135  mp2pm2mp  31136  pmattomply1fo  31138  pmattomply1mhmlem2  31144  lshpkrcl  32857  tendoplcbv  34515  tendo0cbv  34526  tendoicbv  34533  lcfl7N  35242  lcf1o  35292  hdmap1cbv  35544
  Copyright terms: Public domain W3C validator