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

Theorem cbvmptv 4242
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 2524 . 2  |-  F/_ y B
2 nfcv 2524 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4241 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. cmpt 4208
This theorem is referenced by:  onnseq  6543  rdgsucmpt2  6625  frsucmpt2  6634  resixpfo  7037  pw2f1olem  7149  xpmapen  7212  dffi3  7372  ordtypecbv  7420  inf3lema  7513  cantnflem1  7579  cnfcomlem  7590  infxpenc2  7837  fseqenlem1  7839  dfac8a  7845  dfac12r  7960  r1om  8058  fictb  8059  cfsmo  8085  coftr  8087  fin23lem38  8163  compsscnv  8185  isf34lem1  8186  compss  8190  fin1a2lem1  8214  fin1a2lem3  8216  fin1a2lem13  8226  itunisuc  8233  hsmex  8246  domtriom  8257  axdc2  8263  zorn2g  8317  ttukey2g  8330  axdc  8335  konigth  8378  pwcfsdom  8392  canthp1  8463  wunex2  8547  wuncval2  8556  negiso  9917  reexALT  10539  caurcvg2  12399  caucvg  12400  summo  12439  zsum  12440  fsum  12442  ackbijnn  12535  rpnnen  12754  phimullem  13096  eulerth  13100  iserodd  13137  prmreclem5  13216  prmrec  13218  vdwlem7  13283  vdwlem9  13285  vdwlem10  13286  ramub1  13324  ramcl  13325  yonedalem4c  14302  yonedalem3b  14304  gsumwspan  14719  grplactcnv  14815  galactghm  15034  odf1o2  15135  sylow1lem2  15161  sylow1  15165  sylow2b  15185  sylow3lem1  15189  sylow3lem5  15193  sylow3  15195  efgtf  15282  efgsval  15291  ghmcyg  15433  cycsubgcyg  15438  ablfaclem3  15573  ablfac2  15575  fidomndrnglem  16294  mplmonmul  16455  evlslem2  16496  isphld  16809  ordtbaslem  17175  ordtbas2  17178  lly1stc  17481  ptpjopn  17566  xkohmeo  17769  fbasrn  17838  elfm  17901  tmdmulg  18044  tmdgsum  18047  divstgpopn  18071  tsmsfbas  18079  tsmsf1o  18096  ustuqtoplem  18191  utopsnneip  18200  fmucnd  18244  ucnextcn  18256  met1stc  18442  prdsxmslem2  18450  metustto  18474  metustexhalf  18477  metuust  18481  cfilucfil2  18482  metuel  18485  metuel2  18486  metutop  18488  restmetu  18490  metucn  18491  xrge0tsms  18737  metdsge  18751  expcn  18774  pi1xfrcnv  18954  minveclem3b  19197  minveclem5  19202  minvec  19205  ovollb2  19253  ovolshftlem2  19274  ovolscalem2  19278  ovolicc  19287  ioombl1  19324  uniioombllem6  19348  volsup2  19365  vitali  19373  mbfi1fseq  19481  mbfmullem  19485  itg2seq  19502  itg2i1fseq  19515  itg2addlem  19518  itg2cnlem1  19521  itg2cn  19523  dvfsumrlimge0  19782  plyadd  20004  plymul  20005  coeeu  20012  coeid  20025  dvply2g  20070  plydivex  20082  elqaalem2  20105  elqaa  20107  taylthlem1  20157  taylth  20159  pserval  20194  radcnvlem2  20198  radcnvlt2  20203  dvradcnv  20205  pserulm  20206  psercn  20210  pserdvlem2  20212  pserdv  20213  eff1olem  20318  logno1  20395  emcl  20709  harmonicbnd  20710  harmonicbnd2  20711  basel  20740  musum  20844  dchr1  20909  dchrptlem2  20917  dchrpt  20919  lgsqrlem4  20996  lgseisenlem3  21003  2sqlem1  21015  dchrmusumlema  21055  dchrmusum2  21056  dchrvmasumlema  21062  dchrvmasumiflem1  21063  dchrisum0ff  21069  dchrisum0lema  21076  dchrisum0lem1b  21077  dchrisum0lem2a  21079  ubthlem3  22223  minveco  22235  htth  22270  xrge0tsmsd  24053  xrge0mulc1cn  24132  xrge0tmdOLD  24136  gsumesum  24248  esumlub  24249  esumpcvgval  24265  esumcvg  24273  esumcvg2  24274  rrvadd  24490  ballotlemfval  24527  ballotlemi  24538  ballotlemsval  24546  ballotlemsv  24547  ballotlemsf1o  24551  ballotlemrval  24555  ballotlemrinv  24571  derangfmla  24656  erdsze  24668  pconpi1  24704  cvmscbv  24725  cvmsss2  24741  cvmliftlem15  24765  cvmlift2  24783  cvmlift3  24795  relexpsucr  24910  prodmo  25042  zprod  25043  fprod  25047  iprodmul  25089  trpredtr  25258  trpredmintr  25259  bpolyval  25810  sdclem2  26138  prdstotbnd  26195  prdsbnd2  26196  heiborlem10  26221  mzpclval  26474  mzpcompact2lem  26500  rmxyval  26670  dnnumch1  26811  aomclem3  26823  aomclem8  26829  dfac21  26834  pwfi2f1o  26930  expgrowthi  27220  expgrowth  27222  fmuldfeqlem1  27381  itgsin0pilem1  27413  stoweidlem2  27420  stoweidlem17  27435  stoweidlem32  27450  stoweidlem34  27452  stoweidlem43  27461  stirlinglem2  27493  stirlinglem3  27494  stirlinglem8  27499  frgrancvvdeqlemB  27791  frgrancvvdeqlemC  27792  lshpkrcl  29232  tendoplcbv  30890  tendo0cbv  30901  tendoicbv  30908  lcfl7N  31617  lcf1o  31667  hdmap1cbv  31919
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-opab 4209  df-mpt 4210
  Copyright terms: Public domain W3C validator