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

Theorem cbvmptv 4489
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 2566 . 2  |-  F/_ y B
2 nfcv 2566 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4488 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1407    |-> cmpt 4455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-rab 2765  df-v 3063  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-opab 4456  df-mpt 4457
This theorem is referenced by:  fnmptfvd  5970  onnseq  7050  rdgsucmpt2  7135  frsucmpt2  7144  resixpfo  7547  pw2f1olem  7661  xpmapen  7725  dffi3  7927  ordtypecbv  7978  inf3lema  8076  cantnflem1  8142  cantnflem1OLD  8165  cnfcomlem  8177  cnfcomlemOLD  8185  infxpenc2  8433  infxpenc2OLD  8437  fseqenlem1  8439  dfac8a  8445  dfac12r  8560  r1om  8658  fictb  8659  cfsmo  8685  coftr  8687  fin23lem38  8763  compsscnv  8785  isf34lem1  8786  compss  8790  fin1a2lem1  8814  fin1a2lem3  8816  fin1a2lem13  8826  itunisuc  8833  hsmex  8846  domtriom  8857  axdc2  8863  zorn2g  8917  ttukey2g  8930  axdc  8935  konigth  8978  pwcfsdom  8992  canthp1  9064  wunex2  9148  wuncval2  9157  negiso  10561  reexALT  11261  caurcvg2  13651  caucvg  13652  summo  13690  zsum  13691  fsum  13693  ackbijnn  13793  prodmo  13897  zprod  13898  fprod  13902  iprodmul  13950  bpolyval  13996  rpnnen  14171  phimullem  14520  eulerth  14524  iserodd  14570  prmreclem5  14649  prmrec  14651  vdwlem7  14716  vdwlem9  14718  vdwlem10  14719  ramub1  14757  ramcl  14758  yonedalem4c  15872  yonedalem3b  15874  gsumwspan  16340  grplactcnv  16464  galactghm  16754  symgfixfo  16790  pmtrdifwrdel  16836  pmtrdifwrdel2  16837  odf1o2  16919  sylow1lem2  16945  sylow1  16949  sylow2b  16969  sylow3lem1  16973  sylow3lem5  16977  sylow3  16979  efgtf  17066  efgsval  17075  ghmcyg  17224  cycsubgcyg  17229  ablfaclem3  17460  ablfac2  17462  srgbinomlem4  17516  fidomndrnglem  18277  mplmonmul  18448  evlslem2  18502  isphld  18989  frlmphl  19110  mat1ric  19283  mdetralt  19404  smadiadetlem3  19464  pmatcollpw3lem  19578  mp2pm2mplem5  19605  mp2pm2mp  19606  pm2mpmhmlem2  19614  cpmidpmat  19668  cpmadugsumlemF  19671  cpmadugsumfi  19672  cpmadumatpoly  19678  chcoeffeqlem  19680  cayleyhamilton0  19684  cayleyhamilton  19685  cayleyhamiltonALT  19686  cayleyhamilton1  19687  ordtbaslem  19984  ordtbas2  19987  lly1stc  20291  ptpjopn  20407  xkohmeo  20610  fbasrn  20679  elfm  20742  tmdmulg  20885  tmdgsum  20888  qustgpopn  20912  tsmsfbas  20920  tsmsf1o  20941  ustuqtoplem  21036  utopsnneip  21045  fmucnd  21089  ucnextcn  21101  met1stc  21318  prdsxmslem2  21326  metusttoOLD  21354  metustto  21355  metustexhalfOLD  21360  metustexhalf  21361  metuustOLD  21368  metuust  21369  cfilucfil2OLD  21370  cfilucfil2  21371  metuelOLD  21374  metuel  21375  metuel2  21376  metutopOLD  21379  psmetutop  21380  restmetu  21384  metucnOLD  21385  metucn  21386  xrge0tsms  21633  metdsge  21647  expcn  21670  pi1xfrcnv  21851  minveclem3b  22137  minveclem5  22142  minvec  22145  ovollb2  22194  ovolshftlem2  22215  ovolscalem2  22219  ovolicc  22228  ioombl1  22266  uniioombllem6  22291  volsup2  22308  vitali  22316  mbfi1fseq  22422  mbfmullem  22426  itg2seq  22443  itg2i1fseq  22456  itg2addlem  22459  itg2cnlem1  22462  itg2cn  22464  dvfsumrlimge0  22725  plyadd  22908  plymul  22909  coeeu  22916  coeid  22929  dvply2g  22975  plydivex  22987  elqaalem2  23010  elqaa  23012  taylthlem1  23062  taylth  23064  pserval  23099  radcnvlem2  23103  radcnvlt2  23108  dvradcnv  23110  pserulm  23111  psercn  23115  pserdvlem2  23117  pserdv  23118  efgh  23222  eff1olem  23229  circgrp  23233  circsubm  23234  logno1  23313  emcl  23660  harmonicbnd  23661  harmonicbnd2  23662  basel  23746  musum  23850  dchr1  23915  dchrptlem2  23923  dchrpt  23925  lgsqrlem4  24002  lgseisenlem3  24009  2sqlem1  24021  dchrmusumlema  24061  dchrmusum2  24062  dchrvmasumlema  24068  dchrvmasumiflem1  24069  dchrisum0ff  24075  dchrisum0lema  24082  dchrisum0lem1b  24083  dchrisum0lem2a  24085  acopy  24590  wlknwwlknvbij  25169  clwlksizeeq  25281  rusgranumwlkg  25387  frgrancvvdeqlemB  25467  frgrancvvdeqlemC  25468  numclwwlk7  25543  ubthlem3  26215  minveco  26227  htth  26262  xrge0tsmsd  28241  xrge0mulc1cn  28389  xrge0tmdOLD  28393  xrge0tmd  28394  gsumesum  28519  esumlub  28520  esumpcvgval  28538  esumcvg  28546  esumcvg2  28547  eulerpartlems  28818  eulerpart  28840  fibp1  28859  rrvadd  28910  ballotlemfval  28947  ballotlemi  28958  ballotlemsval  28966  ballotlemsv  28967  ballotlemsf1o  28971  ballotlemrval  28975  ballotlemrinv  28991  signsply0  29027  derangfmla  29500  erdsze  29512  pconpi1  29547  cvmscbv  29568  cvmsss2  29584  cvmliftlem15  29608  cvmlift2  29626  cvmlift3  29638  elmrsubrn  29745  iprodefisum  29963  trpredtr  30057  trpredmintr  30058  f1omptsn  31266  mptsnun  31268  fin2so  31425  ftc1anclem5  31480  ftc1anclem6  31481  sdclem2  31530  prdstotbnd  31585  prdsbnd2  31586  heiborlem10  31611  lshpkrcl  32147  tendoplcbv  33807  tendo0cbv  33818  tendoicbv  33825  lcfl7N  34534  lcf1o  34584  hdmap1cbv  34836  mzpclval  35032  mzpcompact2lem  35058  rmxyval  35225  dnnumch1  35365  aomclem3  35377  aomclem8  35382  dfac21  35387  pwfi2f1o  35419  pwfi2f1oOLD  35420  dftrcl3  35712  dfrtrcl3  35725  radcnvrat  36056  expgrowthi  36099  expgrowth  36101  dvradcnv2  36113  binomcxplemradcnv  36118  binomcxplemdvbinom  36119  binomcxplemdvsum  36121  binomcxplemnotnn0  36122  binomcxp  36123  fmuldfeqlem1  36957  sumnnodd  37017  dvsinax  37089  fperdvper  37096  dvcosax  37104  ioodvbdlimc1lem1  37109  ioodvbdlimc1  37111  ioodvbdlimc2  37113  dvnmul  37121  dvnprodlem1  37124  dvnprodlem2  37125  dvnprodlem3  37126  dvnprod  37127  itgsin0pilem1  37129  itgiccshift  37160  stoweidlem2  37165  stoweidlem17  37180  stoweidlem32  37195  stoweidlem34  37197  stoweidlem43  37206  stirlinglem2  37238  stirlinglem3  37239  stirlinglem8  37244  dirkerval  37254  dirkerval2  37257  dirkeritg  37265  dirkercncflem3  37268  dirkercncf  37270  fourierdlem14  37284  fourierdlem18  37288  fourierdlem53  37323  fourierdlem62  37332  fourierdlem71  37341  fourierdlem74  37344  fourierdlem75  37345  fourierdlem76  37346  fourierdlem80  37350  fourierdlem81  37351  fourierdlem84  37354  fourierdlem88  37358  fourierdlem92  37362  fourierdlem93  37363  fourierdlem94  37364  fourierdlem95  37365  fourierdlem96  37366  fourierdlem97  37367  fourierdlem98  37368  fourierdlem99  37369  fourierdlem101  37371  fourierdlem103  37373  fourierdlem104  37374  fourierdlem105  37375  fourierdlem106  37376  fourierdlem107  37377  fourierdlem108  37378  fourierdlem110  37380  fourierdlem111  37381  fourierdlem112  37382  fourierdlem113  37383  fourierdlem115  37385  fouriersw  37395  elaa2  37398  etransclem1  37399  etransclem5  37403  etransclem6  37404  etransclem11  37409  etransclem13  37411  etransclem41  37439  etransclem47  37445  etransc  37447  usgedgvadf1  38057  usgedgvadf1ALT  38060  funcrngcsetcALT  38331  rmsupp0  38485  domnmsuppn0  38486  rmsuppss  38487  suppmptcfin  38496  ply1mulgsum  38514  lcoc0  38547  linc1  38550  lcoel0  38553  lcoss  38561  el0ldep  38591  lincresunit3  38606  isldepslvec2  38610
  Copyright terms: Public domain W3C validator