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

Theorem cbvmptv 4944
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 (𝑥 = 𝑦𝐵 = 𝐶)
Assertion
Ref Expression
cbvmptv (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝑦,𝐵   𝑥,𝐶
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbvmptv
StepHypRef Expression
1 nfcv 2948 . 2 𝑦𝐵
2 nfcv 2948 . 2 𝑥𝐶
3 cbvmptv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbvmpt 4943 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cmpt 4923
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-opab 4907  df-mpt 4924
This theorem is referenced by:  fnmptfvd  6542  onnseq  7677  rdgsucmpt2  7762  frsucmpt2  7771  resixpfo  8183  pw2f1olem  8303  xpmapen  8367  dffi3  8576  ordtypecbv  8661  inf3lema  8768  cantnflem1  8833  cnfcomlem  8843  infxpenc2  9128  fseqenlem1  9130  dfac8a  9136  dfac12r  9253  r1om  9351  fictb  9352  cfsmo  9378  coftr  9380  fin23lem38  9456  compsscnv  9478  isf34lem1  9479  compss  9483  fin1a2lem1  9507  fin1a2lem3  9509  fin1a2lem13  9519  itunisuc  9526  hsmex  9539  domtriom  9550  axdc2  9556  zorn2g  9610  ttukey2g  9623  axdc  9628  konigth  9676  pwcfsdom  9690  canthp1  9761  wunex2  9845  wuncval2  9854  negiso  11288  infrenegsup  11291  rpnnen1  12039  caurcvg2  14631  caucvg  14632  summo  14671  zsum  14672  fsum  14674  ackbijnn  14782  prodmo  14887  zprod  14888  fprod  14892  iprodmul  14954  bpolyval  15000  phimullem  15701  eulerth  15705  iserodd  15757  prmreclem5  15841  prmrec  15843  vdwlem7  15908  vdwlem9  15910  vdwlem10  15911  ramub1  15949  ramcl  15950  yonedalem4c  17122  yonedalem3b  17124  gsumwspan  17588  grplactcnv  17723  galactghm  18024  symgfixfo  18060  pmtrdifwrdel  18106  pmtrdifwrdel2  18107  odf1o2  18189  sylow1lem2  18215  sylow1  18219  sylow2b  18239  sylow3lem1  18243  sylow3lem5  18247  sylow3  18249  efgtf  18336  efgsval  18345  ghmcyg  18498  cycsubgcyg  18503  ablfaclem3  18688  ablfac2  18690  srgbinomlem4  18745  fidomndrnglem  19515  mplmonmul  19673  evlslem2  19720  isphld  20209  frlmphl  20330  mat1ric  20504  mdetralt  20625  smadiadetlem3  20686  pmatcollpw3lem  20801  mp2pm2mplem5  20828  mp2pm2mp  20829  pm2mpmhmlem2  20837  cpmidpmat  20891  cpmadugsumlemF  20894  cpmadugsumfi  20895  cpmadumatpoly  20901  chcoeffeqlem  20903  cayleyhamilton0  20907  cayleyhamilton  20908  cayleyhamiltonALT  20909  cayleyhamilton1  20910  ordtbaslem  21206  ordtbas2  21209  lly1stc  21513  ptpjopn  21629  xkohmeo  21832  fbasrn  21901  elfm  21964  tmdmulg  22109  tmdgsum  22112  qustgpopn  22136  tsmsfbas  22144  tsmsf1o  22161  ustuqtoplem  22256  utopsnneip  22265  fmucnd  22309  ucnextcn  22321  met1stc  22539  prdsxmslem2  22547  metustto  22571  metustexhalf  22574  metuust  22578  cfilucfil2  22579  metuel  22582  metuel2  22583  psmetutop  22585  restmetu  22588  metucn  22589  xrge0tsms  22850  metdsge  22865  expcn  22888  pi1xfrcnv  23069  minveclem3b  23411  minveclem5  23416  minvec  23419  ovollb2  23470  ovolshftlem2  23491  ovolscalem2  23495  ovolicc  23504  ioombl1  23543  uniioombllem6  23569  volsup2  23586  vitali  23594  mbfi1fseq  23702  mbfmullem  23706  itg2seq  23723  itg2i1fseq  23736  itg2addlem  23739  itg2cnlem1  23742  itg2cn  23744  dvfsumrlimge0  24007  plyadd  24187  plymul  24188  coeeu  24195  coeid  24208  dvply2g  24254  plydivex  24266  elqaalem2  24289  elqaa  24291  taylthlem1  24341  taylth  24343  pserval  24378  radcnvlem2  24382  radcnvlt2  24387  dvradcnv  24389  pserulm  24390  psercn  24394  pserdvlem2  24396  pserdv  24397  efgh  24502  eff1olem  24509  circgrp  24513  circsubm  24514  logno1  24596  emcl  24943  harmonicbnd  24944  harmonicbnd2  24945  basel  25030  musum  25131  dchr1  25196  dchrptlem2  25204  dchrpt  25206  lgsqrlem4  25288  lgseisenlem3  25316  2sqlem1  25356  dchrmusumlema  25396  dchrmusum2  25397  dchrvmasumlema  25403  dchrvmasumiflem1  25404  dchrisum0ff  25410  dchrisum0lema  25417  dchrisum0lem1b  25418  dchrisum0lem2a  25420  wlknwwlksnbij  27019  wlksnwwlknvbijOLD  27046  clwlkclwwlken  27155  clwlknf1oclwwlkn  27248  clwlkssizeeqOLD  27250  frgrncvvdeqlem8  27481  frgrncvvdeqlem9  27482  ubthlem3  28056  minveco  28068  htth  28103  xrge0tsmsd  30110  madjusmdetlem2  30219  madjusmdet  30222  xrge0mulc1cn  30312  xrge0tmdOLD  30316  xrge0tmd  30317  gsumesum  30446  esumlub  30447  esumpcvgval  30465  esumcvg  30473  esumcvg2  30474  eulerpartlems  30747  eulerpart  30769  fibp1  30788  rrvadd  30839  ballotlemfval  30876  ballotlemi  30887  ballotlemsval  30895  ballotlemsv  30896  ballotlemsf1o  30900  ballotlemrval  30904  ballotlemrinv  30920  signsply0  30953  actfunsnf1o  31007  actfunsnrndisj  31008  itgexpif  31009  hgt750lemb  31059  derangfmla  31495  erdsze  31507  pconnpi1  31542  cvmscbv  31563  cvmsss2  31579  cvmliftlem15  31603  cvmlift2  31621  cvmlift3  31633  elmrsubrn  31740  iprodefisum  31949  trpredtr  32050  trpredmintr  32051  noeta  32189  knoppcnlem7  32806  knoppf  32843  f1omptsn  33501  mptsnun  33503  fin2so  33709  poimirlem27  33749  broucube  33756  ftc1anclem5  33801  ftc1anclem6  33802  sdclem2  33849  prdstotbnd  33904  prdsbnd2  33905  heiborlem10  33930  lshpkrcl  34896  tendoplcbv  36556  tendo0cbv  36567  tendoicbv  36574  lcfl7N  37282  lcf1o  37332  hdmap1cbv  37583  mzpclval  37790  mzpcompact2lem  37816  rmxyval  37981  dnnumch1  38115  aomclem3  38127  aomclem8  38132  dfac21  38137  pwfi2f1o  38167  dftrcl3  38512  dfrtrcl3  38525  rfovcnvf1od  38798  fsovrfovd  38803  fsovcnvlem  38807  dssmapnvod  38814  clsk3nimkb  38838  radcnvrat  39013  expgrowthi  39032  expgrowth  39034  dvradcnv2  39046  binomcxplemradcnv  39051  binomcxplemdvbinom  39052  binomcxplemdvsum  39054  binomcxplemnotnn0  39055  binomcxp  39056  wessf1ornlem  39860  projf1o  39875  fsumsermpt  40291  fmuldfeqlem1  40294  fprodcn  40312  sumnnodd  40342  limsupvaluz  40420  limsupvaluz2  40450  supcnvlimsup  40452  supcnvlimsupmpt  40453  liminfval2  40480  liminflelimsuplem  40487  fprodsubrecnncnv  40602  fprodaddrecnncnv  40604  dvsinax  40607  fperdvper  40613  dvcosax  40621  ioodvbdlimc1lem1  40626  ioodvbdlimc1  40628  ioodvbdlimc2  40630  dvnmul  40638  dvnprodlem1  40641  dvnprodlem2  40642  dvnprodlem3  40643  dvnprod  40644  itgsin0pilem1  40645  itgiccshift  40675  stoweidlem2  40698  stoweidlem17  40713  stoweidlem32  40728  stoweidlem34  40730  stoweidlem43  40739  stirlinglem2  40771  stirlinglem3  40772  stirlinglem8  40777  dirkerval  40787  dirkerval2  40790  dirkeritg  40798  dirkercncflem3  40801  dirkercncf  40803  fourierdlem14  40817  fourierdlem18  40821  fourierdlem53  40855  fourierdlem62  40864  fourierdlem71  40873  fourierdlem74  40876  fourierdlem75  40877  fourierdlem76  40878  fourierdlem80  40882  fourierdlem81  40883  fourierdlem84  40886  fourierdlem88  40890  fourierdlem92  40894  fourierdlem93  40895  fourierdlem94  40896  fourierdlem95  40897  fourierdlem96  40898  fourierdlem97  40899  fourierdlem98  40900  fourierdlem99  40901  fourierdlem101  40903  fourierdlem103  40905  fourierdlem104  40906  fourierdlem105  40907  fourierdlem106  40908  fourierdlem107  40909  fourierdlem108  40910  fourierdlem110  40912  fourierdlem111  40913  fourierdlem112  40914  fourierdlem113  40915  fourierdlem115  40917  fouriersw  40927  elaa2  40930  etransclem1  40931  etransclem5  40935  etransclem6  40936  etransclem11  40941  etransclem13  40943  etransclem41  40971  etransclem47  40977  etransc  40979  ioorrnopn  41004  ioorrnopnxr  41006  subsaliuncl  41055  sge0resplit  41102  sge0fodjrnlem  41112  nnfoctbdj  41152  iundjiun  41156  voliunsge0lem  41168  meaiuninclem  41176  meaiuninc  41177  meaiininclem  41182  meaiininc  41183  omeiunltfirp  41215  carageniuncllem2  41218  carageniuncl  41219  0ome  41225  isomennd  41227  hoicvrrex  41252  ovn0  41262  ovnsubaddlem2  41267  ovnsubadd  41268  sge0hsphoire  41285  hoidmv1lelem3  41289  hoidmv1le  41290  hoidmvlelem1  41291  hoidmvlelem2  41292  hoidmvlelem3  41293  hoidmvlelem4  41294  hoidmvlelem5  41295  hoidmvle  41296  ovnhoilem2  41298  ovnhoi  41299  hspmbllem2  41323  hspmbl  41325  hoimbl  41327  opnvonmbllem2  41329  ovnsubadd2  41342  ovolval4  41347  ovolval5lem3  41350  ovnovollem3  41354  iccvonmbl  41375  vonioolem2  41377  vonioo  41378  vonicclem2  41380  vonicc  41381  smflimlem4  41464  smfsuplem2  41500  smflimsuplem1  41508  smflimsuplem8  41515  smflimsup  41516  funcrngcsetcALT  42567  rmsupp0  42717  domnmsuppn0  42718  rmsuppss  42719  suppmptcfin  42728  ply1mulgsum  42746  lcoc0  42779  linc1  42782  lcoel0  42785  lcoss  42793  el0ldep  42823  lincresunit3  42838  isldepslvec2  42842  amgmlemALT  43120
  Copyright terms: Public domain W3C validator