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

Theorem cbvmptv 4508
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 2602 . 2  |-  F/_ y B
2 nfcv 2602 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4507 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1454    |-> cmpt 4474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-opab 4475  df-mpt 4476
This theorem is referenced by:  fnmptfvd  6007  onnseq  7088  rdgsucmpt2  7173  frsucmpt2  7182  resixpfo  7585  pw2f1olem  7701  xpmapen  7765  dffi3  7970  ordtypecbv  8057  inf3lema  8154  cantnflem1  8219  cnfcomlem  8229  infxpenc2  8478  fseqenlem1  8480  dfac8a  8486  dfac12r  8601  r1om  8699  fictb  8700  cfsmo  8726  coftr  8728  fin23lem38  8804  compsscnv  8826  isf34lem1  8827  compss  8831  fin1a2lem1  8855  fin1a2lem3  8857  fin1a2lem13  8867  itunisuc  8874  hsmex  8887  domtriom  8898  axdc2  8904  zorn2g  8958  ttukey2g  8971  axdc  8976  konigth  9019  pwcfsdom  9033  canthp1  9104  wunex2  9188  wuncval2  9197  negiso  10614  infrenegsup  10618  reexALT  11324  caurcvg2  13792  caucvg  13793  summo  13831  zsum  13832  fsum  13834  ackbijnn  13934  prodmo  14038  zprod  14039  fprod  14043  iprodmul  14104  bpolyval  14150  rpnnen  14327  phimullem  14775  eulerth  14779  iserodd  14833  prmreclem5  14912  prmrec  14914  vdwlem7  14985  vdwlem9  14987  vdwlem10  14988  ramub1  15034  ramcl  15035  yonedalem4c  16210  yonedalem3b  16212  gsumwspan  16678  grplactcnv  16802  galactghm  17092  symgfixfo  17128  pmtrdifwrdel  17174  pmtrdifwrdel2  17175  odf1o2  17270  sylow1lem2  17299  sylow1  17303  sylow2b  17323  sylow3lem1  17327  sylow3lem5  17331  sylow3  17333  efgtf  17420  efgsval  17429  ghmcyg  17578  cycsubgcyg  17583  ablfaclem3  17768  ablfac2  17770  srgbinomlem4  17824  fidomndrnglem  18578  mplmonmul  18736  evlslem2  18783  isphld  19269  frlmphl  19387  mat1ric  19560  mdetralt  19681  smadiadetlem3  19741  pmatcollpw3lem  19855  mp2pm2mplem5  19882  mp2pm2mp  19883  pm2mpmhmlem2  19891  cpmidpmat  19945  cpmadugsumlemF  19948  cpmadugsumfi  19949  cpmadumatpoly  19955  chcoeffeqlem  19957  cayleyhamilton0  19961  cayleyhamilton  19962  cayleyhamiltonALT  19963  cayleyhamilton1  19964  ordtbaslem  20252  ordtbas2  20255  lly1stc  20559  ptpjopn  20675  xkohmeo  20878  fbasrn  20947  elfm  21010  tmdmulg  21155  tmdgsum  21158  qustgpopn  21182  tsmsfbas  21190  tsmsf1o  21207  ustuqtoplem  21302  utopsnneip  21311  fmucnd  21355  ucnextcn  21367  met1stc  21584  prdsxmslem2  21592  metustto  21616  metustexhalf  21619  metuust  21623  cfilucfil2  21624  metuel  21627  metuel2  21628  psmetutop  21630  restmetu  21633  metucn  21634  xrge0tsms  21900  metdsge  21914  metdsgeOLD  21929  expcn  21952  pi1xfrcnv  22136  minveclem3b  22418  minveclem5  22423  minvec  22426  minveclem3bOLD  22430  minveclem5OLD  22435  minvecOLD  22438  ovollb2  22490  ovolshftlem2  22511  ovolscalem2  22515  ovolicc  22525  ioombl1  22563  uniioombllem6  22594  volsup2  22611  vitali  22619  mbfi1fseq  22727  mbfmullem  22731  itg2seq  22748  itg2i1fseq  22761  itg2addlem  22764  itg2cnlem1  22767  itg2cn  22769  dvfsumrlimge0  23030  plyadd  23219  plymul  23220  coeeu  23227  coeid  23240  dvply2g  23286  plydivex  23298  elqaalem2  23321  elqaalem2OLD  23324  elqaa  23326  taylthlem1  23376  taylth  23378  pserval  23413  radcnvlem2  23417  radcnvlt2  23422  dvradcnv  23424  pserulm  23425  psercn  23429  pserdvlem2  23431  pserdv  23432  efgh  23538  eff1olem  23545  circgrp  23549  circsubm  23550  logno1  23629  emcl  23976  harmonicbnd  23977  harmonicbnd2  23978  basel  24064  musum  24168  dchr1  24233  dchrptlem2  24241  dchrpt  24243  lgsqrlem4  24320  lgseisenlem3  24327  2sqlem1  24339  dchrmusumlema  24379  dchrmusum2  24380  dchrvmasumlema  24386  dchrvmasumiflem1  24387  dchrisum0ff  24393  dchrisum0lema  24400  dchrisum0lem1b  24401  dchrisum0lem2a  24403  wlknwwlknvbij  25516  clwlksizeeq  25628  rusgranumwlkg  25734  frgrancvvdeqlemB  25814  frgrancvvdeqlemC  25815  numclwwlk7  25890  ubthlem3  26562  minveco  26574  minvecoOLD  26584  htth  26619  xrge0tsmsd  28596  madjusmdetlem2  28702  madjusmdet  28705  xrge0mulc1cn  28795  xrge0tmdOLD  28799  xrge0tmd  28800  gsumesum  28928  esumlub  28929  esumpcvgval  28947  esumcvg  28955  esumcvg2  28956  eulerpartlems  29241  eulerpart  29263  fibp1  29282  rrvadd  29333  ballotlemfval  29370  ballotlemi  29381  ballotlemsval  29389  ballotlemsv  29390  ballotlemsf1o  29394  ballotlemrval  29398  ballotlemrinv  29414  ballotlemiOLD  29419  ballotlemsvalOLD  29427  ballotlemsvOLD  29428  ballotlemsf1oOLD  29432  ballotlemrvalOLD  29436  ballotlemrinvOLD  29452  signsply0  29488  derangfmla  29961  erdsze  29973  pconpi1  30008  cvmscbv  30029  cvmsss2  30045  cvmliftlem15  30069  cvmlift2  30087  cvmlift3  30099  elmrsubrn  30206  iprodefisum  30425  trpredtr  30519  trpredmintr  30520  f1omptsn  31783  mptsnun  31785  fin2so  31976  poimirlem27  32011  broucube  32018  ftc1anclem5  32065  ftc1anclem6  32066  sdclem2  32115  prdstotbnd  32170  prdsbnd2  32171  heiborlem10  32196  lshpkrcl  32726  tendoplcbv  34386  tendo0cbv  34397  tendoicbv  34404  lcfl7N  35113  lcf1o  35163  hdmap1cbv  35415  mzpclval  35611  mzpcompact2lem  35637  rmxyval  35807  dnnumch1  35946  aomclem3  35958  aomclem8  35963  dfac21  35968  pwfi2f1o  35998  dftrcl3  36356  dfrtrcl3  36369  radcnvrat  36706  expgrowthi  36725  expgrowth  36727  dvradcnv2  36739  binomcxplemradcnv  36744  binomcxplemdvbinom  36745  binomcxplemdvsum  36747  binomcxplemnotnn0  36748  binomcxp  36749  wessf1ornlem  37496  projf1o  37511  fmuldfeqlem1  37697  sumnnodd  37747  dvsinax  37820  fperdvper  37827  dvcosax  37835  ioodvbdlimc1lem1  37840  ioodvbdlimc1lem1OLD  37842  ioodvbdlimc1  37844  ioodvbdlimc2  37847  dvnmul  37855  dvnprodlem1  37858  dvnprodlem2  37859  dvnprodlem3  37860  dvnprod  37861  itgsin0pilem1  37863  itgiccshift  37894  stoweidlem2  37899  stoweidlem17  37914  stoweidlem32  37930  stoweidlem34  37932  stoweidlem43  37941  stirlinglem2  37974  stirlinglem3  37975  stirlinglem8  37980  dirkerval  37990  dirkerval2  37993  dirkeritg  38001  dirkercncflem3  38004  dirkercncf  38006  fourierdlem14  38020  fourierdlem18  38024  fourierdlem53  38060  fourierdlem62  38069  fourierdlem71  38078  fourierdlem74  38081  fourierdlem75  38082  fourierdlem76  38083  fourierdlem80  38087  fourierdlem81  38088  fourierdlem84  38091  fourierdlem88  38095  fourierdlem92  38099  fourierdlem93  38100  fourierdlem94  38101  fourierdlem95  38102  fourierdlem96  38103  fourierdlem97  38104  fourierdlem98  38105  fourierdlem99  38106  fourierdlem101  38108  fourierdlem103  38110  fourierdlem104  38111  fourierdlem105  38112  fourierdlem106  38113  fourierdlem107  38114  fourierdlem108  38115  fourierdlem110  38117  fourierdlem111  38118  fourierdlem112  38119  fourierdlem113  38120  fourierdlem115  38122  fouriersw  38132  elaa2  38136  etransclem1  38137  etransclem5  38141  etransclem6  38142  etransclem11  38147  etransclem13  38149  etransclem41  38177  etransclem47  38183  etransc  38186  sge0resplit  38285  sge0fodjrnlem  38295  nnfoctbdj  38331  iundjiun  38335  omeiunltfirp  38377  carageniuncllem2  38380  carageniuncl  38381  0ome  38387  isomennd  38389  hoicvrrex  38415  ovn0  38425  ovnsubaddlem2  38430  ovnsubadd  38431  sge0hsphoire  38448  hoidmv1lelem3  38452  hoidmv1le  38453  hoidmvlelem1  38454  hoidmvlelem2  38455  hoidmvlelem3  38456  hoidmvlelem4  38457  hoidmvlelem5  38458  hoidmvle  38459  ovnhoilem2  38461  ovnhoi  38462  hspmbllem2  38486  hspmbl  38488  hoimbl  38490  opnvonmbllem2  38492  usgedgvadf1  39999  usgedgvadf1ALT  40002  funcrngcsetcALT  40273  rmsupp0  40425  domnmsuppn0  40426  rmsuppss  40427  suppmptcfin  40436  ply1mulgsum  40454  lcoc0  40487  linc1  40490  lcoel0  40493  lcoss  40501  el0ldep  40531  lincresunit3  40546  isldepslvec2  40550
  Copyright terms: Public domain W3C validator