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

Theorem cbvmptv 4113
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 2421 . 2  |-  F/_ y B
2 nfcv 2421 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4112 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    e. cmpt 4079
This theorem is referenced by:  onnseq  6363  rdgsucmpt2  6445  frsucmpt2  6454  resixpfo  6856  pw2f1olem  6968  xpmapen  7031  dffi3  7186  ordtypecbv  7234  inf3lema  7327  cantnflem1  7393  cnfcomlem  7404  infxpenc2  7651  fseqenlem1  7653  dfac8a  7659  dfac12r  7774  r1om  7872  fictb  7873  cfsmo  7899  coftr  7901  fin23lem38  7977  compsscnv  7999  isf34lem1  8000  compss  8004  fin1a2lem1  8028  fin1a2lem3  8030  fin1a2lem13  8040  itunisuc  8047  hsmex  8060  domtriom  8071  axdc2  8077  zorn2g  8132  ttukey2g  8145  axdc  8150  konigth  8193  pwcfsdom  8207  canthp1  8278  wunex2  8362  wuncval2  8371  negiso  9732  reexALT  10350  caurcvg2  12152  caucvg  12153  summo  12192  zsum  12193  fsum  12195  ackbijnn  12288  rpnnen  12507  phimullem  12849  eulerth  12853  iserodd  12890  prmreclem5  12969  prmrec  12971  vdwlem7  13036  vdwlem9  13038  vdwlem10  13039  ramub1  13077  ramcl  13078  yonedalem4c  14053  yonedalem3b  14055  gsumwspan  14470  grplactcnv  14566  galactghm  14785  odf1o2  14886  sylow1lem2  14912  sylow1  14916  sylow2b  14936  sylow3lem1  14940  sylow3lem5  14944  sylow3  14946  efgtf  15033  efgsval  15042  ghmcyg  15184  cycsubgcyg  15189  ablfaclem3  15324  ablfac2  15326  fidomndrnglem  16049  mplmonmul  16210  evlslem2  16251  isphld  16560  ordtbaslem  16920  ordtbas2  16923  lly1stc  17224  ptpjopn  17308  xkohmeo  17508  fbasrn  17581  elfm  17644  tmdmulg  17777  tmdgsum  17780  divstgpopn  17804  tsmsfbas  17812  tsmsf1o  17829  met1stc  18069  prdsxmslem2  18077  xrge0tsms  18341  metdsge  18355  expcn  18378  pi1xfrcnv  18557  minveclem3b  18794  minveclem5  18799  minvec  18802  ovollb2  18850  ovolshftlem2  18871  ovolscalem2  18875  ovolicc  18884  ioombl1  18921  uniioombllem6  18945  volsup2  18962  vitali  18970  mbfi1fseq  19078  mbfmullem  19082  itg2seq  19099  itg2i1fseq  19112  itg2addlem  19115  itg2cnlem1  19118  itg2cn  19120  dvfsumrlimge0  19379  plyadd  19601  plymul  19602  coeeu  19609  coeid  19622  dvply2g  19667  plydivex  19679  elqaalem2  19702  elqaa  19704  taylthlem1  19754  taylth  19756  pserval  19788  radcnvlem2  19792  radcnvlt2  19797  dvradcnv  19799  pserulm  19800  psercn  19804  pserdvlem2  19806  pserdv  19807  eff1olem  19912  logno1  19985  emcl  20298  harmonicbnd  20299  harmonicbnd2  20300  basel  20329  musum  20433  dchr1  20498  dchrptlem2  20506  dchrpt  20508  lgsqrlem4  20585  lgseisenlem3  20592  2sqlem1  20604  dchrmusumlema  20644  dchrmusum2  20645  dchrvmasumlema  20651  dchrvmasumiflem1  20652  dchrisum0ff  20658  dchrisum0lema  20665  dchrisum0lem1b  20666  dchrisum0lem2a  20668  ubthlem3  21453  minveco  21465  htth  21500  ballotlemfval  23050  ballotlemsf1o  23074  xrge0tsmsd  23384  esumpcvgval  23448  esumcvg2  23457  derangfmla  23723  erdsze  23735  pconpi1  23770  cvmscbv  23791  cvmsss2  23807  cvmliftlem15  23831  cvmlift2  23849  cvmlift3  23861  relexpsucr  24028  trpredtr  24235  trpredmintr  24236  bpolyval  24786  trinv  25406  cmprtr  25407  cmprtr2  25408  ltrinvlem  25417  cmpltr2  25418  cmprltr2  25422  cnvtr  25627  sdclem2  26463  prdstotbnd  26529  prdsbnd2  26530  heiborlem10  26555  mzpclval  26814  mzpcompact2lem  26840  rmxyval  27011  dnnumch1  27152  aomclem3  27164  aomclem8  27170  dfac21  27175  pwfi2f1o  27271  expgrowthi  27561  expgrowth  27563  stoweidlem2  27762  stoweidlem17  27777  stoweidlem32  27792  stoweidlem34  27794  stoweidlem43  27803  stoweidlem44  27804  lshpkrcl  29379  tendoplcbv  31037  tendo0cbv  31048  tendoicbv  31055  lcfl7N  31764  lcf1o  31814  hdmap1cbv  32066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-opab 4080  df-mpt 4081
  Copyright terms: Public domain W3C validator