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

Theorem cbvmptv 4234
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 2516 . 2  |-  F/_ y B
2 nfcv 2516 . 2  |-  F/_ x C
3 cbvmptv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbvmpt 4233 1  |-  ( x  e.  A  |->  B )  =  ( y  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. cmpt 4200
This theorem is referenced by:  onnseq  6535  rdgsucmpt2  6617  frsucmpt2  6626  resixpfo  7029  pw2f1olem  7141  xpmapen  7204  dffi3  7364  ordtypecbv  7412  inf3lema  7505  cantnflem1  7571  cnfcomlem  7582  infxpenc2  7829  fseqenlem1  7831  dfac8a  7837  dfac12r  7952  r1om  8050  fictb  8051  cfsmo  8077  coftr  8079  fin23lem38  8155  compsscnv  8177  isf34lem1  8178  compss  8182  fin1a2lem1  8206  fin1a2lem3  8208  fin1a2lem13  8218  itunisuc  8225  hsmex  8238  domtriom  8249  axdc2  8255  zorn2g  8309  ttukey2g  8322  axdc  8327  konigth  8370  pwcfsdom  8384  canthp1  8455  wunex2  8539  wuncval2  8548  negiso  9909  reexALT  10531  caurcvg2  12391  caucvg  12392  summo  12431  zsum  12432  fsum  12434  ackbijnn  12527  rpnnen  12746  phimullem  13088  eulerth  13092  iserodd  13129  prmreclem5  13208  prmrec  13210  vdwlem7  13275  vdwlem9  13277  vdwlem10  13278  ramub1  13316  ramcl  13317  yonedalem4c  14294  yonedalem3b  14296  gsumwspan  14711  grplactcnv  14807  galactghm  15026  odf1o2  15127  sylow1lem2  15153  sylow1  15157  sylow2b  15177  sylow3lem1  15181  sylow3lem5  15185  sylow3  15187  efgtf  15274  efgsval  15283  ghmcyg  15425  cycsubgcyg  15430  ablfaclem3  15565  ablfac2  15567  fidomndrnglem  16286  mplmonmul  16447  evlslem2  16488  isphld  16801  ordtbaslem  17167  ordtbas2  17170  lly1stc  17473  ptpjopn  17558  xkohmeo  17761  fbasrn  17830  elfm  17893  tmdmulg  18036  tmdgsum  18039  divstgpopn  18063  tsmsfbas  18071  tsmsf1o  18088  ustuqtoplem  18183  utopsnneip  18192  fmucnd  18236  ucnextcn  18248  met1stc  18434  prdsxmslem2  18442  metustto  18466  metustexhalf  18469  metuust  18473  cfilucfil2  18474  metuel  18477  metuel2  18478  metutop  18480  restmetu  18482  metucn  18483  xrge0tsms  18729  metdsge  18743  expcn  18766  pi1xfrcnv  18946  minveclem3b  19189  minveclem5  19194  minvec  19197  ovollb2  19245  ovolshftlem2  19266  ovolscalem2  19270  ovolicc  19279  ioombl1  19316  uniioombllem6  19340  volsup2  19357  vitali  19365  mbfi1fseq  19473  mbfmullem  19477  itg2seq  19494  itg2i1fseq  19507  itg2addlem  19510  itg2cnlem1  19513  itg2cn  19515  dvfsumrlimge0  19774  plyadd  19996  plymul  19997  coeeu  20004  coeid  20017  dvply2g  20062  plydivex  20074  elqaalem2  20097  elqaa  20099  taylthlem1  20149  taylth  20151  pserval  20186  radcnvlem2  20190  radcnvlt2  20195  dvradcnv  20197  pserulm  20198  psercn  20202  pserdvlem2  20204  pserdv  20205  eff1olem  20310  logno1  20387  emcl  20701  harmonicbnd  20702  harmonicbnd2  20703  basel  20732  musum  20836  dchr1  20901  dchrptlem2  20909  dchrpt  20911  lgsqrlem4  20988  lgseisenlem3  20995  2sqlem1  21007  dchrmusumlema  21047  dchrmusum2  21048  dchrvmasumlema  21054  dchrvmasumiflem1  21055  dchrisum0ff  21061  dchrisum0lema  21068  dchrisum0lem1b  21069  dchrisum0lem2a  21071  ubthlem3  22215  minveco  22227  htth  22262  xrge0tsmsd  24045  xrge0mulc1cn  24124  xrge0tmdOLD  24128  gsumesum  24240  esumlub  24241  esumpcvgval  24257  esumcvg  24265  esumcvg2  24266  rrvadd  24482  ballotlemfval  24519  ballotlemi  24530  ballotlemsval  24538  ballotlemsv  24539  ballotlemsf1o  24543  ballotlemrval  24547  ballotlemrinv  24563  derangfmla  24648  erdsze  24660  pconpi1  24696  cvmscbv  24717  cvmsss2  24733  cvmliftlem15  24757  cvmlift2  24775  cvmlift3  24787  relexpsucr  24902  prodmo  25034  zprod  25035  fprod  25039  iprodmul  25081  trpredtr  25250  trpredmintr  25251  bpolyval  25802  sdclem2  26130  prdstotbnd  26187  prdsbnd2  26188  heiborlem10  26213  mzpclval  26466  mzpcompact2lem  26492  rmxyval  26662  dnnumch1  26803  aomclem3  26815  aomclem8  26821  dfac21  26826  pwfi2f1o  26922  expgrowthi  27212  expgrowth  27214  fmuldfeqlem1  27373  itgsin0pilem1  27405  stoweidlem2  27412  stoweidlem17  27427  stoweidlem32  27442  stoweidlem34  27444  stoweidlem43  27453  stirlinglem2  27485  stirlinglem3  27486  stirlinglem8  27491  frgrancvvdeqlemB  27783  frgrancvvdeqlemC  27784  lshpkrcl  29282  tendoplcbv  30940  tendo0cbv  30951  tendoicbv  30958  lcfl7N  31667  lcf1o  31717  hdmap1cbv  31969
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-opab 4201  df-mpt 4202
  Copyright terms: Public domain W3C validator