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

Theorem cbvmptv 4260
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 2540 . 2  |-  F/_ y B
2 nfcv 2540 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4259 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. cmpt 4226
This theorem is referenced by:  onnseq  6565  rdgsucmpt2  6647  frsucmpt2  6656  resixpfo  7059  pw2f1olem  7171  xpmapen  7234  dffi3  7394  ordtypecbv  7442  inf3lema  7535  cantnflem1  7601  cnfcomlem  7612  infxpenc2  7859  fseqenlem1  7861  dfac8a  7867  dfac12r  7982  r1om  8080  fictb  8081  cfsmo  8107  coftr  8109  fin23lem38  8185  compsscnv  8207  isf34lem1  8208  compss  8212  fin1a2lem1  8236  fin1a2lem3  8238  fin1a2lem13  8248  itunisuc  8255  hsmex  8268  domtriom  8279  axdc2  8285  zorn2g  8339  ttukey2g  8352  axdc  8357  konigth  8400  pwcfsdom  8414  canthp1  8485  wunex2  8569  wuncval2  8578  negiso  9940  reexALT  10562  caurcvg2  12426  caucvg  12427  summo  12466  zsum  12467  fsum  12469  ackbijnn  12562  rpnnen  12781  phimullem  13123  eulerth  13127  iserodd  13164  prmreclem5  13243  prmrec  13245  vdwlem7  13310  vdwlem9  13312  vdwlem10  13313  ramub1  13351  ramcl  13352  yonedalem4c  14329  yonedalem3b  14331  gsumwspan  14746  grplactcnv  14842  galactghm  15061  odf1o2  15162  sylow1lem2  15188  sylow1  15192  sylow2b  15212  sylow3lem1  15216  sylow3lem5  15220  sylow3  15222  efgtf  15309  efgsval  15318  ghmcyg  15460  cycsubgcyg  15465  ablfaclem3  15600  ablfac2  15602  fidomndrnglem  16321  mplmonmul  16482  evlslem2  16523  isphld  16840  ordtbaslem  17206  ordtbas2  17209  lly1stc  17512  ptpjopn  17597  xkohmeo  17800  fbasrn  17869  elfm  17932  tmdmulg  18075  tmdgsum  18078  divstgpopn  18102  tsmsfbas  18110  tsmsf1o  18127  ustuqtoplem  18222  utopsnneip  18231  fmucnd  18275  ucnextcn  18287  met1stc  18504  prdsxmslem2  18512  metusttoOLD  18540  metustto  18541  metustexhalfOLD  18546  metustexhalf  18547  metuustOLD  18554  metuust  18555  cfilucfil2OLD  18556  cfilucfil2  18557  metuelOLD  18560  metuel  18561  metuel2  18562  metutopOLD  18565  psmetutop  18566  restmetu  18570  metucnOLD  18571  metucn  18572  xrge0tsms  18818  metdsge  18832  expcn  18855  pi1xfrcnv  19035  minveclem3b  19282  minveclem5  19287  minvec  19290  ovollb2  19338  ovolshftlem2  19359  ovolscalem2  19363  ovolicc  19372  ioombl1  19409  uniioombllem6  19433  volsup2  19450  vitali  19458  mbfi1fseq  19566  mbfmullem  19570  itg2seq  19587  itg2i1fseq  19600  itg2addlem  19603  itg2cnlem1  19606  itg2cn  19608  dvfsumrlimge0  19867  plyadd  20089  plymul  20090  coeeu  20097  coeid  20110  dvply2g  20155  plydivex  20167  elqaalem2  20190  elqaa  20192  taylthlem1  20242  taylth  20244  pserval  20279  radcnvlem2  20283  radcnvlt2  20288  dvradcnv  20290  pserulm  20291  psercn  20295  pserdvlem2  20297  pserdv  20298  eff1olem  20403  logno1  20480  emcl  20794  harmonicbnd  20795  harmonicbnd2  20796  basel  20825  musum  20929  dchr1  20994  dchrptlem2  21002  dchrpt  21004  lgsqrlem4  21081  lgseisenlem3  21088  2sqlem1  21100  dchrmusumlema  21140  dchrmusum2  21141  dchrvmasumlema  21147  dchrvmasumiflem1  21148  dchrisum0ff  21154  dchrisum0lema  21161  dchrisum0lem1b  21162  dchrisum0lem2a  21164  ubthlem3  22327  minveco  22339  htth  22374  xrge0tsmsd  24176  xrge0mulc1cn  24280  xrge0tmdOLD  24284  gsumesum  24404  esumlub  24405  esumpcvgval  24421  esumcvg  24429  esumcvg2  24430  rrvadd  24663  ballotlemfval  24700  ballotlemi  24711  ballotlemsval  24719  ballotlemsv  24720  ballotlemsf1o  24724  ballotlemrval  24728  ballotlemrinv  24744  derangfmla  24829  erdsze  24841  pconpi1  24877  cvmscbv  24898  cvmsss2  24914  cvmliftlem15  24938  cvmlift2  24956  cvmlift3  24968  relexpsucr  25083  prodmo  25215  zprod  25216  fprod  25220  iprodmul  25269  iprodefisum  25271  trpredtr  25447  trpredmintr  25448  bpolyval  25999  sdclem2  26336  prdstotbnd  26393  prdsbnd2  26394  heiborlem10  26419  mzpclval  26672  mzpcompact2lem  26698  rmxyval  26868  dnnumch1  27009  aomclem3  27021  aomclem8  27027  dfac21  27032  pwfi2f1o  27128  expgrowthi  27418  expgrowth  27420  fmuldfeqlem1  27579  itgsin0pilem1  27611  stoweidlem2  27618  stoweidlem17  27633  stoweidlem32  27648  stoweidlem34  27650  stoweidlem43  27659  stirlinglem2  27691  stirlinglem3  27692  stirlinglem8  27697  frgrancvvdeqlemB  28141  frgrancvvdeqlemC  28142  lshpkrcl  29599  tendoplcbv  31257  tendo0cbv  31268  tendoicbv  31275  lcfl7N  31984  lcf1o  32034  hdmap1cbv  32286
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-opab 4227  df-mpt 4228
  Copyright terms: Public domain W3C validator