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

Theorem cbvmptv 4538
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 2629 . 2  |-  F/_ y B
2 nfcv 2629 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4537 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    |-> cmpt 4505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-opab 4506  df-mpt 4507
This theorem is referenced by:  fnmptfvd  5984  onnseq  7015  rdgsucmpt2  7096  frsucmpt2  7105  resixpfo  7507  pw2f1olem  7621  xpmapen  7685  dffi3  7891  ordtypecbv  7942  inf3lema  8041  cantnflem1  8108  cantnflem1OLD  8131  cnfcomlem  8143  cnfcomlemOLD  8151  infxpenc2  8399  infxpenc2OLD  8403  fseqenlem1  8405  dfac8a  8411  dfac12r  8526  r1om  8624  fictb  8625  cfsmo  8651  coftr  8653  fin23lem38  8729  compsscnv  8751  isf34lem1  8752  compss  8756  fin1a2lem1  8780  fin1a2lem3  8782  fin1a2lem13  8792  itunisuc  8799  hsmex  8812  domtriom  8823  axdc2  8829  zorn2g  8883  ttukey2g  8896  axdc  8901  konigth  8944  pwcfsdom  8958  canthp1  9032  wunex2  9116  wuncval2  9125  negiso  10519  reexALT  11214  caurcvg2  13463  caucvg  13464  summo  13502  zsum  13503  fsum  13505  ackbijnn  13603  rpnnen  13821  phimullem  14168  eulerth  14172  iserodd  14218  prmreclem5  14297  prmrec  14299  vdwlem7  14364  vdwlem9  14366  vdwlem10  14367  ramub1  14405  ramcl  14406  yonedalem4c  15404  yonedalem3b  15406  gsumwspan  15846  grplactcnv  15948  galactghm  16233  symgfixfo  16270  pmtrdifwrdel  16316  pmtrdifwrdel2  16317  odf1o2  16399  sylow1lem2  16425  sylow1  16429  sylow2b  16449  sylow3lem1  16453  sylow3lem5  16457  sylow3  16459  efgtf  16546  efgsval  16555  ghmcyg  16701  cycsubgcyg  16706  ablfaclem3  16940  ablfac2  16942  srgbinomlem4  16996  fidomndrnglem  17754  mplmonmul  17925  evlslem2  17979  isphld  18484  frlmphl  18607  mat1ric  18784  mdetralt  18905  smadiadetlem3  18965  pmatcollpw3lem  19079  mp2pm2mplem5  19106  mp2pm2mp  19107  pm2mpmhmlem2  19115  cpmidpmat  19169  cpmadugsumlemF  19172  cpmadugsumfi  19173  cpmadumatpoly  19179  chcoeffeqlem  19181  cayleyhamilton0  19185  cayleyhamilton  19186  cayleyhamiltonALT  19187  cayleyhamilton1  19188  ordtbaslem  19483  ordtbas2  19486  lly1stc  19791  ptpjopn  19876  xkohmeo  20079  fbasrn  20148  elfm  20211  tmdmulg  20354  tmdgsum  20357  divstgpopn  20381  tsmsfbas  20389  tsmsf1o  20410  ustuqtoplem  20505  utopsnneip  20514  fmucnd  20558  ucnextcn  20570  met1stc  20787  prdsxmslem2  20795  metusttoOLD  20823  metustto  20824  metustexhalfOLD  20829  metustexhalf  20830  metuustOLD  20837  metuust  20838  cfilucfil2OLD  20839  cfilucfil2  20840  metuelOLD  20843  metuel  20844  metuel2  20845  metutopOLD  20848  psmetutop  20849  restmetu  20853  metucnOLD  20854  metucn  20855  xrge0tsms  21102  metdsge  21116  expcn  21139  pi1xfrcnv  21320  minveclem3b  21606  minveclem5  21611  minvec  21614  ovollb2  21663  ovolshftlem2  21684  ovolscalem2  21688  ovolicc  21697  ioombl1  21735  uniioombllem6  21760  volsup2  21777  vitali  21785  mbfi1fseq  21891  mbfmullem  21895  itg2seq  21912  itg2i1fseq  21925  itg2addlem  21928  itg2cnlem1  21931  itg2cn  21933  dvfsumrlimge0  22194  plyadd  22377  plymul  22378  coeeu  22385  coeid  22398  dvply2g  22443  plydivex  22455  elqaalem2  22478  elqaa  22480  taylthlem1  22530  taylth  22532  pserval  22567  radcnvlem2  22571  radcnvlt2  22576  dvradcnv  22578  pserulm  22579  psercn  22583  pserdvlem2  22585  pserdv  22586  eff1olem  22696  logno1  22773  emcl  23088  harmonicbnd  23089  harmonicbnd2  23090  basel  23119  musum  23223  dchr1  23288  dchrptlem2  23296  dchrpt  23298  lgsqrlem4  23375  lgseisenlem3  23382  2sqlem1  23394  dchrmusumlema  23434  dchrmusum2  23435  dchrvmasumlema  23441  dchrvmasumiflem1  23442  dchrisum0ff  23448  dchrisum0lema  23455  dchrisum0lem1b  23456  dchrisum0lem2a  23458  wlknwwlknvbij  24444  clwlksizeeq  24556  rusgranumwlkg  24662  frgrancvvdeqlemB  24743  frgrancvvdeqlemC  24744  numclwwlk7  24819  ubthlem3  25492  minveco  25504  htth  25539  xrge0tsmsd  27466  xrge0mulc1cn  27587  xrge0tmdOLD  27591  gsumesum  27735  esumlub  27736  esumpcvgval  27752  esumcvg  27760  esumcvg2  27761  eulerpartlems  27967  eulerpart  27989  fibp1  28008  rrvadd  28059  ballotlemfval  28096  ballotlemi  28107  ballotlemsval  28115  ballotlemsv  28116  ballotlemsf1o  28120  ballotlemrval  28124  ballotlemrinv  28140  signsply0  28176  derangfmla  28302  erdsze  28314  pconpi1  28350  cvmscbv  28371  cvmsss2  28387  cvmliftlem15  28411  cvmlift2  28429  cvmlift3  28441  relexpsucr  28556  prodmo  28673  zprod  28674  fprod  28678  iprodmul  28727  iprodefisum  28729  trpredtr  28918  trpredmintr  28919  bpolyval  29416  fin2so  29645  ftc1anclem5  29699  ftc1anclem6  29700  sdclem2  29866  prdstotbnd  29921  prdsbnd2  29922  heiborlem10  29947  mzpclval  30289  mzpcompact2lem  30316  rmxyval  30483  dnnumch1  30622  aomclem3  30634  aomclem8  30639  dfac21  30644  pwfi2f1o  30676  expgrowthi  30866  expgrowth  30868  fmuldfeqlem1  31160  sumnnodd  31200  fperdvper  31276  dvcosax  31284  ioodvbdlimc1lem1  31289  ioodvbdlimc1  31291  ioodvbdlimc2  31293  itgsin0pilem1  31295  stoweidlem2  31330  stoweidlem17  31345  stoweidlem32  31360  stoweidlem34  31362  stoweidlem43  31371  stirlinglem2  31403  stirlinglem3  31404  stirlinglem8  31409  dirkeritg  31430  fourierdlem14  31449  fourierdlem18  31453  fourierdlem45  31480  fourierdlem53  31488  fourierdlem62  31497  fourierdlem71  31506  fourierdlem74  31509  fourierdlem75  31510  fourierdlem76  31511  fourierdlem78  31513  fourierdlem80  31515  fourierdlem83  31518  fourierdlem84  31519  fourierdlem88  31523  fourierdlem94  31529  fourierdlem95  31530  fourierdlem96  31531  fourierdlem97  31532  fourierdlem98  31533  fourierdlem99  31534  fourierdlem103  31538  fourierdlem104  31539  fourierdlem105  31540  fourierdlem106  31541  fourierdlem107  31542  fourierdlem108  31543  fourierdlem110  31545  fourierdlem111  31546  fourierdlem112  31547  fourierdlem113  31548  fourierdlem115  31550  fouriersw  31560  usgedgvadf1  31910  usgedgvadf1ALT  31913  rmsupp0  32060  domnmsuppn0  32061  rmsuppss  32062  suppmptcfin  32071  ply1mulgsum  32089  lcoc0  32122  linc1  32125  lcoel0  32128  lcoss  32136  el0ldep  32166  lincresunit3  32181  isldepslvec2  32185  lshpkrcl  33931  tendoplcbv  35589  tendo0cbv  35600  tendoicbv  35607  lcfl7N  36316  lcf1o  36366  hdmap1cbv  36618
  Copyright terms: Public domain W3C validator