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

Theorem cbvmptv 4302
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 2574 . 2  |-  F/_ y B
2 nfcv 2574 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4301 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. cmpt 4268
This theorem is referenced by:  onnseq  6608  rdgsucmpt2  6690  frsucmpt2  6699  resixpfo  7102  pw2f1olem  7214  xpmapen  7277  dffi3  7438  ordtypecbv  7488  inf3lema  7581  cantnflem1  7647  cnfcomlem  7658  infxpenc2  7905  fseqenlem1  7907  dfac8a  7913  dfac12r  8028  r1om  8126  fictb  8127  cfsmo  8153  coftr  8155  fin23lem38  8231  compsscnv  8253  isf34lem1  8254  compss  8258  fin1a2lem1  8282  fin1a2lem3  8284  fin1a2lem13  8294  itunisuc  8301  hsmex  8314  domtriom  8325  axdc2  8331  zorn2g  8385  ttukey2g  8398  axdc  8403  konigth  8446  pwcfsdom  8460  canthp1  8531  wunex2  8615  wuncval2  8624  negiso  9986  reexALT  10608  caurcvg2  12473  caucvg  12474  summo  12513  zsum  12514  fsum  12516  ackbijnn  12609  rpnnen  12828  phimullem  13170  eulerth  13174  iserodd  13211  prmreclem5  13290  prmrec  13292  vdwlem7  13357  vdwlem9  13359  vdwlem10  13360  ramub1  13398  ramcl  13399  yonedalem4c  14376  yonedalem3b  14378  gsumwspan  14793  grplactcnv  14889  galactghm  15108  odf1o2  15209  sylow1lem2  15235  sylow1  15239  sylow2b  15259  sylow3lem1  15263  sylow3lem5  15267  sylow3  15269  efgtf  15356  efgsval  15365  ghmcyg  15507  cycsubgcyg  15512  ablfaclem3  15647  ablfac2  15649  fidomndrnglem  16368  mplmonmul  16529  evlslem2  16570  isphld  16887  ordtbaslem  17254  ordtbas2  17257  lly1stc  17561  ptpjopn  17646  xkohmeo  17849  fbasrn  17918  elfm  17981  tmdmulg  18124  tmdgsum  18127  divstgpopn  18151  tsmsfbas  18159  tsmsf1o  18176  ustuqtoplem  18271  utopsnneip  18280  fmucnd  18324  ucnextcn  18336  met1stc  18553  prdsxmslem2  18561  metusttoOLD  18589  metustto  18590  metustexhalfOLD  18595  metustexhalf  18596  metuustOLD  18603  metuust  18604  cfilucfil2OLD  18605  cfilucfil2  18606  metuelOLD  18609  metuel  18610  metuel2  18611  metutopOLD  18614  psmetutop  18615  restmetu  18619  metucnOLD  18620  metucn  18621  xrge0tsms  18867  metdsge  18881  expcn  18904  pi1xfrcnv  19084  minveclem3b  19331  minveclem5  19336  minvec  19339  ovollb2  19387  ovolshftlem2  19408  ovolscalem2  19412  ovolicc  19421  ioombl1  19458  uniioombllem6  19482  volsup2  19499  vitali  19507  mbfi1fseq  19615  mbfmullem  19619  itg2seq  19636  itg2i1fseq  19649  itg2addlem  19652  itg2cnlem1  19655  itg2cn  19657  dvfsumrlimge0  19916  plyadd  20138  plymul  20139  coeeu  20146  coeid  20159  dvply2g  20204  plydivex  20216  elqaalem2  20239  elqaa  20241  taylthlem1  20291  taylth  20293  pserval  20328  radcnvlem2  20332  radcnvlt2  20337  dvradcnv  20339  pserulm  20340  psercn  20344  pserdvlem2  20346  pserdv  20347  eff1olem  20452  logno1  20529  emcl  20843  harmonicbnd  20844  harmonicbnd2  20845  basel  20874  musum  20978  dchr1  21043  dchrptlem2  21051  dchrpt  21053  lgsqrlem4  21130  lgseisenlem3  21137  2sqlem1  21149  dchrmusumlema  21189  dchrmusum2  21190  dchrvmasumlema  21196  dchrvmasumiflem1  21197  dchrisum0ff  21203  dchrisum0lema  21210  dchrisum0lem1b  21211  dchrisum0lem2a  21213  ubthlem3  22376  minveco  22388  htth  22423  xrge0tsmsd  24225  xrge0mulc1cn  24329  xrge0tmdOLD  24333  gsumesum  24453  esumlub  24454  esumpcvgval  24470  esumcvg  24478  esumcvg2  24479  rrvadd  24712  ballotlemfval  24749  ballotlemi  24760  ballotlemsval  24768  ballotlemsv  24769  ballotlemsf1o  24773  ballotlemrval  24777  ballotlemrinv  24793  derangfmla  24878  erdsze  24890  pconpi1  24926  cvmscbv  24947  cvmsss2  24963  cvmliftlem15  24987  cvmlift2  25005  cvmlift3  25017  relexpsucr  25132  prodmo  25264  zprod  25265  fprod  25269  iprodmul  25318  iprodefisum  25320  trpredtr  25510  trpredmintr  25511  bpolyval  26097  ftc1anclem5  26286  ftc1anclem6  26287  sdclem2  26448  prdstotbnd  26505  prdsbnd2  26506  heiborlem10  26531  mzpclval  26784  mzpcompact2lem  26810  rmxyval  26980  dnnumch1  27121  aomclem3  27133  aomclem8  27138  dfac21  27143  pwfi2f1o  27239  expgrowthi  27529  expgrowth  27531  fmuldfeqlem1  27690  itgsin0pilem1  27722  stoweidlem2  27729  stoweidlem17  27744  stoweidlem32  27759  stoweidlem34  27761  stoweidlem43  27770  stirlinglem2  27802  stirlinglem3  27803  stirlinglem8  27808  frgrancvvdeqlemB  28489  frgrancvvdeqlemC  28490  lshpkrcl  29976  tendoplcbv  31634  tendo0cbv  31645  tendoicbv  31652  lcfl7N  32361  lcf1o  32411  hdmap1cbv  32663
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-opab 4269  df-mpt 4270
  Copyright terms: Public domain W3C validator