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

Theorem cbvmptv 4127
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 2432 . 2  |-  F/_ y B
2 nfcv 2432 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4126 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. cmpt 4093
This theorem is referenced by:  onnseq  6377  rdgsucmpt2  6459  frsucmpt2  6468  resixpfo  6870  pw2f1olem  6982  xpmapen  7045  dffi3  7200  ordtypecbv  7248  inf3lema  7341  cantnflem1  7407  cnfcomlem  7418  infxpenc2  7665  fseqenlem1  7667  dfac8a  7673  dfac12r  7788  r1om  7886  fictb  7887  cfsmo  7913  coftr  7915  fin23lem38  7991  compsscnv  8013  isf34lem1  8014  compss  8018  fin1a2lem1  8042  fin1a2lem3  8044  fin1a2lem13  8054  itunisuc  8061  hsmex  8074  domtriom  8085  axdc2  8091  zorn2g  8146  ttukey2g  8159  axdc  8164  konigth  8207  pwcfsdom  8221  canthp1  8292  wunex2  8376  wuncval2  8385  negiso  9746  reexALT  10364  caurcvg2  12166  caucvg  12167  summo  12206  zsum  12207  fsum  12209  ackbijnn  12302  rpnnen  12521  phimullem  12863  eulerth  12867  iserodd  12904  prmreclem5  12983  prmrec  12985  vdwlem7  13050  vdwlem9  13052  vdwlem10  13053  ramub1  13091  ramcl  13092  yonedalem4c  14067  yonedalem3b  14069  gsumwspan  14484  grplactcnv  14580  galactghm  14799  odf1o2  14900  sylow1lem2  14926  sylow1  14930  sylow2b  14950  sylow3lem1  14954  sylow3lem5  14958  sylow3  14960  efgtf  15047  efgsval  15056  ghmcyg  15198  cycsubgcyg  15203  ablfaclem3  15338  ablfac2  15340  fidomndrnglem  16063  mplmonmul  16224  evlslem2  16265  isphld  16574  ordtbaslem  16934  ordtbas2  16937  lly1stc  17238  ptpjopn  17322  xkohmeo  17522  fbasrn  17595  elfm  17658  tmdmulg  17791  tmdgsum  17794  divstgpopn  17818  tsmsfbas  17826  tsmsf1o  17843  met1stc  18083  prdsxmslem2  18091  xrge0tsms  18355  metdsge  18369  expcn  18392  pi1xfrcnv  18571  minveclem3b  18808  minveclem5  18813  minvec  18816  ovollb2  18864  ovolshftlem2  18885  ovolscalem2  18889  ovolicc  18898  ioombl1  18935  uniioombllem6  18959  volsup2  18976  vitali  18984  mbfi1fseq  19092  mbfmullem  19096  itg2seq  19113  itg2i1fseq  19126  itg2addlem  19129  itg2cnlem1  19132  itg2cn  19134  dvfsumrlimge0  19393  plyadd  19615  plymul  19616  coeeu  19623  coeid  19636  dvply2g  19681  plydivex  19693  elqaalem2  19716  elqaa  19718  taylthlem1  19768  taylth  19770  pserval  19802  radcnvlem2  19806  radcnvlt2  19811  dvradcnv  19813  pserulm  19814  psercn  19818  pserdvlem2  19820  pserdv  19821  eff1olem  19926  logno1  19999  emcl  20312  harmonicbnd  20313  harmonicbnd2  20314  basel  20343  musum  20447  dchr1  20512  dchrptlem2  20520  dchrpt  20522  lgsqrlem4  20599  lgseisenlem3  20606  2sqlem1  20618  dchrmusumlema  20658  dchrmusum2  20659  dchrvmasumlema  20665  dchrvmasumiflem1  20666  dchrisum0ff  20672  dchrisum0lema  20679  dchrisum0lem1b  20680  dchrisum0lem2a  20682  ubthlem3  21467  minveco  21479  htth  21514  ballotlemfval  23064  ballotlemsf1o  23088  xrge0tsmsd  23397  esumpcvgval  23461  esumcvg2  23470  derangfmla  23736  erdsze  23748  pconpi1  23783  cvmscbv  23804  cvmsss2  23820  cvmliftlem15  23844  cvmlift2  23862  cvmlift3  23874  relexpsucr  24041  prodmo  24159  zprod  24160  fprod  24164  trpredtr  24304  trpredmintr  24305  bpolyval  24856  trinv  25498  cmprtr  25499  cmprtr2  25500  ltrinvlem  25509  cmpltr2  25510  cmprltr2  25514  cnvtr  25719  sdclem2  26555  prdstotbnd  26621  prdsbnd2  26622  heiborlem10  26647  mzpclval  26906  mzpcompact2lem  26932  rmxyval  27103  dnnumch1  27244  aomclem3  27256  aomclem8  27262  dfac21  27267  pwfi2f1o  27363  expgrowthi  27653  expgrowth  27655  stoweidlem2  27854  stoweidlem17  27869  stoweidlem32  27884  stoweidlem34  27886  stoweidlem43  27895  stoweidlem44  27896  lshpkrcl  29928  tendoplcbv  31586  tendo0cbv  31597  tendoicbv  31604  lcfl7N  32313  lcf1o  32363  hdmap1cbv  32615
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-opab 4094  df-mpt 4095
  Copyright terms: Public domain W3C validator