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

Theorem cbvmptv 4111
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 2419 . 2  |-  F/_ y B
2 nfcv 2419 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4110 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. cmpt 4077
This theorem is referenced by:  onnseq  6361  rdgsucmpt2  6443  frsucmpt2  6452  resixpfo  6854  pw2f1olem  6966  xpmapen  7029  dffi3  7184  ordtypecbv  7232  inf3lema  7325  cantnflem1  7391  cnfcomlem  7402  infxpenc2  7649  fseqenlem1  7651  dfac8a  7657  dfac12r  7772  r1om  7870  fictb  7871  cfsmo  7897  coftr  7899  fin23lem38  7975  compsscnv  7997  isf34lem1  7998  compss  8002  fin1a2lem1  8026  fin1a2lem3  8028  fin1a2lem13  8038  itunisuc  8045  hsmex  8058  domtriom  8069  axdc2  8075  zorn2g  8130  ttukey2g  8143  axdc  8148  konigth  8191  pwcfsdom  8205  canthp1  8276  wunex2  8360  wuncval2  8369  negiso  9730  reexALT  10348  caurcvg2  12150  caucvg  12151  summo  12190  zsum  12191  fsum  12193  ackbijnn  12286  rpnnen  12505  phimullem  12847  eulerth  12851  iserodd  12888  prmreclem5  12967  prmrec  12969  vdwlem7  13034  vdwlem9  13036  vdwlem10  13037  ramub1  13075  ramcl  13076  yonedalem4c  14051  yonedalem3b  14053  gsumwspan  14468  grplactcnv  14564  galactghm  14783  odf1o2  14884  sylow1lem2  14910  sylow1  14914  sylow2b  14934  sylow3lem1  14938  sylow3lem5  14942  sylow3  14944  efgtf  15031  efgsval  15040  ghmcyg  15182  cycsubgcyg  15187  ablfaclem3  15322  ablfac2  15324  fidomndrnglem  16047  mplmonmul  16208  evlslem2  16249  isphld  16558  ordtbaslem  16918  ordtbas2  16921  lly1stc  17222  ptpjopn  17306  xkohmeo  17506  fbasrn  17579  elfm  17642  tmdmulg  17775  tmdgsum  17778  divstgpopn  17802  tsmsfbas  17810  tsmsf1o  17827  met1stc  18067  prdsxmslem2  18075  xrge0tsms  18339  metdsge  18353  expcn  18376  pi1xfrcnv  18555  minveclem3b  18792  minveclem5  18797  minvec  18800  ovollb2  18848  ovolshftlem2  18869  ovolscalem2  18873  ovolicc  18882  ioombl1  18919  uniioombllem6  18943  volsup2  18960  vitali  18968  mbfi1fseq  19076  mbfmullem  19080  itg2seq  19097  itg2i1fseq  19110  itg2addlem  19113  itg2cnlem1  19116  itg2cn  19118  dvfsumrlimge0  19377  plyadd  19599  plymul  19600  coeeu  19607  coeid  19620  dvply2g  19665  plydivex  19677  elqaalem2  19700  elqaa  19702  taylthlem1  19752  taylth  19754  pserval  19786  radcnvlem2  19790  radcnvlt2  19795  dvradcnv  19797  pserulm  19798  psercn  19802  pserdvlem2  19804  pserdv  19805  eff1olem  19910  logno1  19983  emcl  20296  harmonicbnd  20297  harmonicbnd2  20298  basel  20327  musum  20431  dchr1  20496  dchrptlem2  20504  dchrpt  20506  lgsqrlem4  20583  lgseisenlem3  20590  2sqlem1  20602  dchrmusumlema  20642  dchrmusum2  20643  dchrvmasumlema  20649  dchrvmasumiflem1  20650  dchrisum0ff  20656  dchrisum0lema  20663  dchrisum0lem1b  20664  dchrisum0lem2a  20666  ubthlem3  21451  minveco  21463  htth  21498  ballotlemfval  23048  ballotlemsf1o  23072  xrge0tsmsd  23382  esumpcvgval  23446  esumcvg2  23455  derangfmla  23721  erdsze  23733  pconpi1  23768  cvmscbv  23789  cvmsss2  23805  cvmliftlem15  23829  cvmlift2  23847  cvmlift3  23859  relexpsucr  24026  trpredtr  24233  trpredmintr  24234  bpolyval  24784  trinv  25395  cmprtr  25396  cmprtr2  25397  ltrinvlem  25406  cmpltr2  25407  cmprltr2  25411  cnvtr  25616  sdclem2  26452  prdstotbnd  26518  prdsbnd2  26519  heiborlem10  26544  mzpclval  26803  mzpcompact2lem  26829  rmxyval  27000  dnnumch1  27141  aomclem3  27153  aomclem8  27159  dfac21  27164  pwfi2f1o  27260  expgrowthi  27550  expgrowth  27552  stoweidlem2  27751  stoweidlem17  27766  stoweidlem32  27781  stoweidlem34  27783  stoweidlem43  27792  stoweidlem44  27793  lshpkrcl  29306  tendoplcbv  30964  tendo0cbv  30975  tendoicbv  30982  lcfl7N  31691  lcf1o  31741  hdmap1cbv  31993
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-mpt 4079
  Copyright terms: Public domain W3C validator