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

Theorem cbvmptv 4514
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 2585 . 2  |-  F/_ y B
2 nfcv 2585 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4513 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1438    |-> cmpt 4480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-opab 4481  df-mpt 4482
This theorem is referenced by:  fnmptfvd  5998  onnseq  7069  rdgsucmpt2  7154  frsucmpt2  7163  resixpfo  7566  pw2f1olem  7680  xpmapen  7744  dffi3  7949  ordtypecbv  8036  inf3lema  8133  cantnflem1  8197  cnfcomlem  8207  infxpenc2  8455  fseqenlem1  8457  dfac8a  8463  dfac12r  8578  r1om  8676  fictb  8677  cfsmo  8703  coftr  8705  fin23lem38  8781  compsscnv  8803  isf34lem1  8804  compss  8808  fin1a2lem1  8832  fin1a2lem3  8834  fin1a2lem13  8844  itunisuc  8851  hsmex  8864  domtriom  8875  axdc2  8881  zorn2g  8935  ttukey2g  8948  axdc  8953  konigth  8996  pwcfsdom  9010  canthp1  9081  wunex2  9165  wuncval2  9174  negiso  10589  infrenegsup  10593  reexALT  11298  caurcvg2  13737  caucvg  13738  summo  13776  zsum  13777  fsum  13779  ackbijnn  13879  prodmo  13983  zprod  13984  fprod  13988  iprodmul  14049  bpolyval  14095  rpnnen  14272  phimullem  14720  eulerth  14724  iserodd  14778  prmreclem5  14857  prmrec  14859  vdwlem7  14930  vdwlem9  14932  vdwlem10  14933  ramub1  14979  ramcl  14980  yonedalem4c  16155  yonedalem3b  16157  gsumwspan  16623  grplactcnv  16747  galactghm  17037  symgfixfo  17073  pmtrdifwrdel  17119  pmtrdifwrdel2  17120  odf1o2  17215  sylow1lem2  17244  sylow1  17248  sylow2b  17268  sylow3lem1  17272  sylow3lem5  17276  sylow3  17278  efgtf  17365  efgsval  17374  ghmcyg  17523  cycsubgcyg  17528  ablfaclem3  17713  ablfac2  17715  srgbinomlem4  17769  fidomndrnglem  18523  mplmonmul  18681  evlslem2  18728  isphld  19213  frlmphl  19331  mat1ric  19504  mdetralt  19625  smadiadetlem3  19685  pmatcollpw3lem  19799  mp2pm2mplem5  19826  mp2pm2mp  19827  pm2mpmhmlem2  19835  cpmidpmat  19889  cpmadugsumlemF  19892  cpmadugsumfi  19893  cpmadumatpoly  19899  chcoeffeqlem  19901  cayleyhamilton0  19905  cayleyhamilton  19906  cayleyhamiltonALT  19907  cayleyhamilton1  19908  ordtbaslem  20196  ordtbas2  20199  lly1stc  20503  ptpjopn  20619  xkohmeo  20822  fbasrn  20891  elfm  20954  tmdmulg  21099  tmdgsum  21102  qustgpopn  21126  tsmsfbas  21134  tsmsf1o  21151  ustuqtoplem  21246  utopsnneip  21255  fmucnd  21299  ucnextcn  21311  met1stc  21528  prdsxmslem2  21536  metustto  21560  metustexhalf  21563  metuust  21567  cfilucfil2  21568  metuel  21571  metuel2  21572  psmetutop  21574  restmetu  21577  metucn  21578  xrge0tsms  21844  metdsge  21858  metdsgeOLD  21873  expcn  21896  pi1xfrcnv  22080  minveclem3b  22362  minveclem5  22367  minvec  22370  minveclem3bOLD  22374  minveclem5OLD  22379  minvecOLD  22382  ovollb2  22434  ovolshftlem2  22455  ovolscalem2  22459  ovolicc  22469  ioombl1  22507  uniioombllem6  22538  volsup2  22555  vitali  22563  mbfi1fseq  22671  mbfmullem  22675  itg2seq  22692  itg2i1fseq  22705  itg2addlem  22708  itg2cnlem1  22711  itg2cn  22713  dvfsumrlimge0  22974  plyadd  23163  plymul  23164  coeeu  23171  coeid  23184  dvply2g  23230  plydivex  23242  elqaalem2  23265  elqaalem2OLD  23268  elqaa  23270  taylthlem1  23320  taylth  23322  pserval  23357  radcnvlem2  23361  radcnvlt2  23366  dvradcnv  23368  pserulm  23369  psercn  23373  pserdvlem2  23375  pserdv  23376  efgh  23482  eff1olem  23489  circgrp  23493  circsubm  23494  logno1  23573  emcl  23920  harmonicbnd  23921  harmonicbnd2  23922  basel  24008  musum  24112  dchr1  24177  dchrptlem2  24185  dchrpt  24187  lgsqrlem4  24264  lgseisenlem3  24271  2sqlem1  24283  dchrmusumlema  24323  dchrmusum2  24324  dchrvmasumlema  24330  dchrvmasumiflem1  24331  dchrisum0ff  24337  dchrisum0lema  24344  dchrisum0lem1b  24345  dchrisum0lem2a  24347  wlknwwlknvbij  25460  clwlksizeeq  25572  rusgranumwlkg  25678  frgrancvvdeqlemB  25758  frgrancvvdeqlemC  25759  numclwwlk7  25834  ubthlem3  26506  minveco  26518  minvecoOLD  26528  htth  26563  xrge0tsmsd  28550  madjusmdetlem2  28656  madjusmdet  28659  xrge0mulc1cn  28749  xrge0tmdOLD  28753  xrge0tmd  28754  gsumesum  28882  esumlub  28883  esumpcvgval  28901  esumcvg  28909  esumcvg2  28910  eulerpartlems  29195  eulerpart  29217  fibp1  29236  rrvadd  29287  ballotlemfval  29324  ballotlemi  29335  ballotlemsval  29343  ballotlemsv  29344  ballotlemsf1o  29348  ballotlemrval  29352  ballotlemrinv  29368  ballotlemiOLD  29373  ballotlemsvalOLD  29381  ballotlemsvOLD  29382  ballotlemsf1oOLD  29386  ballotlemrvalOLD  29390  ballotlemrinvOLD  29406  signsply0  29442  derangfmla  29915  erdsze  29927  pconpi1  29962  cvmscbv  29983  cvmsss2  29999  cvmliftlem15  30023  cvmlift2  30041  cvmlift3  30053  elmrsubrn  30160  iprodefisum  30378  trpredtr  30472  trpredmintr  30473  f1omptsn  31686  mptsnun  31688  fin2so  31852  poimirlem27  31887  broucube  31894  ftc1anclem5  31941  ftc1anclem6  31942  sdclem2  31991  prdstotbnd  32046  prdsbnd2  32047  heiborlem10  32072  lshpkrcl  32607  tendoplcbv  34267  tendo0cbv  34278  tendoicbv  34285  lcfl7N  34994  lcf1o  35044  hdmap1cbv  35296  mzpclval  35492  mzpcompact2lem  35518  rmxyval  35689  dnnumch1  35828  aomclem3  35840  aomclem8  35845  dfac21  35850  pwfi2f1o  35880  dftrcl3  36178  dfrtrcl3  36191  radcnvrat  36527  expgrowthi  36546  expgrowth  36548  dvradcnv2  36560  binomcxplemradcnv  36565  binomcxplemdvbinom  36566  binomcxplemdvsum  36568  binomcxplemnotnn0  36569  binomcxp  36570  wessf1ornlem  37315  projf1o  37330  fmuldfeqlem1  37486  sumnnodd  37536  dvsinax  37609  fperdvper  37616  dvcosax  37624  ioodvbdlimc1lem1  37629  ioodvbdlimc1lem1OLD  37631  ioodvbdlimc1  37633  ioodvbdlimc2  37636  dvnmul  37644  dvnprodlem1  37647  dvnprodlem2  37648  dvnprodlem3  37649  dvnprod  37650  itgsin0pilem1  37652  itgiccshift  37683  stoweidlem2  37688  stoweidlem17  37703  stoweidlem32  37719  stoweidlem34  37721  stoweidlem43  37730  stirlinglem2  37763  stirlinglem3  37764  stirlinglem8  37769  dirkerval  37779  dirkerval2  37782  dirkeritg  37790  dirkercncflem3  37793  dirkercncf  37795  fourierdlem14  37809  fourierdlem18  37813  fourierdlem53  37849  fourierdlem62  37858  fourierdlem71  37867  fourierdlem74  37870  fourierdlem75  37871  fourierdlem76  37872  fourierdlem80  37876  fourierdlem81  37877  fourierdlem84  37880  fourierdlem88  37884  fourierdlem92  37888  fourierdlem93  37889  fourierdlem94  37890  fourierdlem95  37891  fourierdlem96  37892  fourierdlem97  37893  fourierdlem98  37894  fourierdlem99  37895  fourierdlem101  37897  fourierdlem103  37899  fourierdlem104  37900  fourierdlem105  37901  fourierdlem106  37902  fourierdlem107  37903  fourierdlem108  37904  fourierdlem110  37906  fourierdlem111  37907  fourierdlem112  37908  fourierdlem113  37909  fourierdlem115  37911  fouriersw  37921  elaa2  37925  etransclem1  37926  etransclem5  37930  etransclem6  37931  etransclem11  37936  etransclem13  37938  etransclem41  37966  etransclem47  37972  etransc  37975  sge0resplit  38042  sge0fodjrnlem  38052  nnfoctbdj  38079  iundjiun  38083  omeiunltfirp  38125  carageniuncllem2  38128  carageniuncl  38129  0ome  38135  isomennd  38137  hoicvrrex  38159  ovn0  38169  ovnsubaddlem2  38174  ovnsubadd  38175  usgedgvadf1  39031  usgedgvadf1ALT  39034  funcrngcsetcALT  39305  rmsupp0  39459  domnmsuppn0  39460  rmsuppss  39461  suppmptcfin  39470  ply1mulgsum  39488  lcoc0  39521  linc1  39524  lcoel0  39527  lcoss  39535  el0ldep  39565  lincresunit3  39580  isldepslvec2  39584
  Copyright terms: Public domain W3C validator