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

Theorem cbvmptv 4292
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 2571 . 2  |-  F/_ y B
2 nfcv 2571 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4291 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. cmpt 4258
This theorem is referenced by:  onnseq  6598  rdgsucmpt2  6680  frsucmpt2  6689  resixpfo  7092  pw2f1olem  7204  xpmapen  7267  dffi3  7428  ordtypecbv  7478  inf3lema  7571  cantnflem1  7637  cnfcomlem  7648  infxpenc2  7895  fseqenlem1  7897  dfac8a  7903  dfac12r  8018  r1om  8116  fictb  8117  cfsmo  8143  coftr  8145  fin23lem38  8221  compsscnv  8243  isf34lem1  8244  compss  8248  fin1a2lem1  8272  fin1a2lem3  8274  fin1a2lem13  8284  itunisuc  8291  hsmex  8304  domtriom  8315  axdc2  8321  zorn2g  8375  ttukey2g  8388  axdc  8393  konigth  8436  pwcfsdom  8450  canthp1  8521  wunex2  8605  wuncval2  8614  negiso  9976  reexALT  10598  caurcvg2  12463  caucvg  12464  summo  12503  zsum  12504  fsum  12506  ackbijnn  12599  rpnnen  12818  phimullem  13160  eulerth  13164  iserodd  13201  prmreclem5  13280  prmrec  13282  vdwlem7  13347  vdwlem9  13349  vdwlem10  13350  ramub1  13388  ramcl  13389  yonedalem4c  14366  yonedalem3b  14368  gsumwspan  14783  grplactcnv  14879  galactghm  15098  odf1o2  15199  sylow1lem2  15225  sylow1  15229  sylow2b  15249  sylow3lem1  15253  sylow3lem5  15257  sylow3  15259  efgtf  15346  efgsval  15355  ghmcyg  15497  cycsubgcyg  15502  ablfaclem3  15637  ablfac2  15639  fidomndrnglem  16358  mplmonmul  16519  evlslem2  16560  isphld  16877  ordtbaslem  17244  ordtbas2  17247  lly1stc  17551  ptpjopn  17636  xkohmeo  17839  fbasrn  17908  elfm  17971  tmdmulg  18114  tmdgsum  18117  divstgpopn  18141  tsmsfbas  18149  tsmsf1o  18166  ustuqtoplem  18261  utopsnneip  18270  fmucnd  18314  ucnextcn  18326  met1stc  18543  prdsxmslem2  18551  metusttoOLD  18579  metustto  18580  metustexhalfOLD  18585  metustexhalf  18586  metuustOLD  18593  metuust  18594  cfilucfil2OLD  18595  cfilucfil2  18596  metuelOLD  18599  metuel  18600  metuel2  18601  metutopOLD  18604  psmetutop  18605  restmetu  18609  metucnOLD  18610  metucn  18611  xrge0tsms  18857  metdsge  18871  expcn  18894  pi1xfrcnv  19074  minveclem3b  19321  minveclem5  19326  minvec  19329  ovollb2  19377  ovolshftlem2  19398  ovolscalem2  19402  ovolicc  19411  ioombl1  19448  uniioombllem6  19472  volsup2  19489  vitali  19497  mbfi1fseq  19605  mbfmullem  19609  itg2seq  19626  itg2i1fseq  19639  itg2addlem  19642  itg2cnlem1  19645  itg2cn  19647  dvfsumrlimge0  19906  plyadd  20128  plymul  20129  coeeu  20136  coeid  20149  dvply2g  20194  plydivex  20206  elqaalem2  20229  elqaa  20231  taylthlem1  20281  taylth  20283  pserval  20318  radcnvlem2  20322  radcnvlt2  20327  dvradcnv  20329  pserulm  20330  psercn  20334  pserdvlem2  20336  pserdv  20337  eff1olem  20442  logno1  20519  emcl  20833  harmonicbnd  20834  harmonicbnd2  20835  basel  20864  musum  20968  dchr1  21033  dchrptlem2  21041  dchrpt  21043  lgsqrlem4  21120  lgseisenlem3  21127  2sqlem1  21139  dchrmusumlema  21179  dchrmusum2  21180  dchrvmasumlema  21186  dchrvmasumiflem1  21187  dchrisum0ff  21193  dchrisum0lema  21200  dchrisum0lem1b  21201  dchrisum0lem2a  21203  ubthlem3  22366  minveco  22378  htth  22413  xrge0tsmsd  24215  xrge0mulc1cn  24319  xrge0tmdOLD  24323  gsumesum  24443  esumlub  24444  esumpcvgval  24460  esumcvg  24468  esumcvg2  24469  rrvadd  24702  ballotlemfval  24739  ballotlemi  24750  ballotlemsval  24758  ballotlemsv  24759  ballotlemsf1o  24763  ballotlemrval  24767  ballotlemrinv  24783  derangfmla  24868  erdsze  24880  pconpi1  24916  cvmscbv  24937  cvmsss2  24953  cvmliftlem15  24977  cvmlift2  24995  cvmlift3  25007  relexpsucr  25122  prodmo  25254  zprod  25255  fprod  25259  iprodmul  25308  iprodefisum  25310  trpredtr  25500  trpredmintr  25501  bpolyval  26087  ftc1anclem5  26274  ftc1anclem6  26275  sdclem2  26437  prdstotbnd  26494  prdsbnd2  26495  heiborlem10  26520  mzpclval  26773  mzpcompact2lem  26799  rmxyval  26969  dnnumch1  27110  aomclem3  27122  aomclem8  27127  dfac21  27132  pwfi2f1o  27228  expgrowthi  27518  expgrowth  27520  fmuldfeqlem1  27679  itgsin0pilem1  27711  stoweidlem2  27718  stoweidlem17  27733  stoweidlem32  27748  stoweidlem34  27750  stoweidlem43  27759  stirlinglem2  27791  stirlinglem3  27792  stirlinglem8  27797  frgrancvvdeqlemB  28364  frgrancvvdeqlemC  28365  lshpkrcl  29851  tendoplcbv  31509  tendo0cbv  31520  tendoicbv  31527  lcfl7N  32236  lcf1o  32286  hdmap1cbv  32538
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-opab 4259  df-mpt 4260
  Copyright terms: Public domain W3C validator