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

Theorem fvres 6101
Description: The value of a restricted function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fvres (𝐴𝐵 → ((𝐹𝐵)‘𝐴) = (𝐹𝐴))

Proof of Theorem fvres
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 vex 3175 . . . . 5 𝑥 ∈ V
21brres 5309 . . . 4 (𝐴(𝐹𝐵)𝑥 ↔ (𝐴𝐹𝑥𝐴𝐵))
32rbaib 944 . . 3 (𝐴𝐵 → (𝐴(𝐹𝐵)𝑥𝐴𝐹𝑥))
43iotabidv 5774 . 2 (𝐴𝐵 → (℩𝑥𝐴(𝐹𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5 df-fv 5797 . 2 ((𝐹𝐵)‘𝐴) = (℩𝑥𝐴(𝐹𝐵)𝑥)
6 df-fv 5797 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
74, 5, 63eqtr4g 2668 1 (𝐴𝐵 → ((𝐹𝐵)‘𝐴) = (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976   class class class wbr 4577  cres 5029  cio 5751  cfv 5789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pr 4827
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-xp 5033  df-res 5039  df-iota 5753  df-fv 5797
This theorem is referenced by:  fvresd  6102  funssfv  6103  fveqres  6124  feqresmpt  6144  dffv2  6165  fvreseq0  6209  respreima  6236  fveqressseq  6247  ffvresb  6285  fnressn  6307  fressnfv  6309  fvressn  6311  fvresi  6321  fvsnun1  6330  fvsnun2  6331  fsnunfv  6335  funfvima  6373  resfvresima  6375  funiunfv  6387  soisores  6454  isores3  6462  isoini2  6466  ovres  6675  ofres  6788  f1oweALT  7020  offres  7031  fo1stres  7060  fo2ndres  7061  curry1  7133  curry2  7136  fparlem1  7141  fparlem2  7142  fo2ndf  7148  f1o2ndf1  7149  fnsuppres  7186  wfrlem4  7282  smores  7313  smores2  7315  tfrlem1  7336  tz7.44-2  7367  fr0g  7395  frsuc  7396  tz7.48lem  7400  seqomlem1  7409  seqomlem2  7410  seqomlem3  7411  seqomlem4  7412  onasuc  7472  onmsuc  7473  onesuc  7474  resixp  7806  fofinf1o  8103  ixpfi2  8124  ordtypelem4  8286  ordtypelem6  8288  ordtypelem7  8289  unxpwdom2  8353  cantnfres  8434  cantnfp1lem3  8437  dfac12lem1  8825  ackbij2lem2  8922  ackbij2lem3  8923  cfsmolem  8952  alephsing  8958  ttukeylem3  9193  fpwwe2lem6  9313  fpwwe2lem8  9315  fpwwe2lem9  9316  canthp1lem2  9331  inar1  9453  addpiord  9562  mulpiord  9563  addpqnq  9616  mulpqnq  9619  fseq1p1m1  12240  injresinj  12408  seqfeq2  12643  seqres  12647  seqf1olem2  12660  hashgval  12939  hashinf  12941  hashgval2  12982  hashf1lem1  13050  seqcoll  13059  swrdccat1  13257  shftidt  13618  rlimres  14085  lo1res  14086  climres  14102  isercolllem3  14193  fsumss  14251  isumclim3  14280  fsum2dlem  14291  ackbijnn  14347  fprodss  14465  fprod2dlem  14497  iprodclim3  14518  bpolylem  14566  fprodefsum  14612  reeff1  14637  bitsf1  14954  sadcaddlem  14965  sadcadd  14966  sadadd2  14968  sadaddlem  14974  sadasslem  14978  sadeq  14980  eucalgcvga  15085  eucalg  15086  unbenlem  15398  strfv2d  15681  setsid  15690  setsnid  15691  funcres  16327  dmaf  16470  cdaf  16471  1stf1  16603  2ndf1  16606  1stfcl  16608  2ndfcl  16609  prf1st  16615  prf2nd  16616  1st2ndprf  16617  uncf2  16648  diag12  16655  diag2  16656  curf2ndf  16658  yonedalem22  16689  lubval  16755  glbval  16768  resmhm  17130  resghm  17447  efgsres  17922  efgredlemd  17928  efgredlem  17931  gsumzaddlem  18092  dprdfadd  18190  dprdres  18198  dmdprdsplitlem  18207  dprdcntz2  18208  dmdprdsplit2lem  18215  dprdsplit  18218  dpjidcl  18228  ablfac1eu  18243  mgpf  18330  prdscrngd  18384  abvres  18610  reslmhm  18821  ltbwe  19241  subrgascl  19267  subrgasclcl  19268  znf1o  19666  znunithash  19679  psgndiflemB  19712  smadiadetlem3  20240  cnpresti  20849  cnprest  20850  lmres  20861  tx1cn  21169  tx2cn  21170  upxp  21183  uptx  21185  ptrescn  21199  txkgen  21212  cnmpt1st  21228  cnmpt2nd  21229  ptuncnv  21367  ptunhmeo  21368  cnextfres1  21629  prdstmdd  21684  prdsxmslem2  22091  subgnm2  22195  remetdval  22347  rescncf  22455  isncvsngp  22701  lmle  22851  lmcau  22863  ovoliunlem1  23021  ovolicc2lem4  23039  mblvol  23049  mbflimsup  23183  limcdif  23390  limcres  23400  dvreslem  23423  dvres2lem  23424  dvlip  23504  dvlipcn  23505  dvlip2  23506  c1liplem1  23507  c1lip1  23508  c1lip3  23510  dvgt0lem1  23513  dvivthlem1  23519  lhop1lem  23524  lhop  23527  dvcnvrelem1  23528  dvcvx  23531  ftc2ditglem  23556  itgsubstlem  23559  plyreres  23786  plyexmo  23816  aannenlem1  23831  taylthlem2  23876  ulmres  23890  ulmss  23899  psercn  23928  pserdvlem2  23930  reeff1o  23949  reefiso  23950  efcvx  23951  reefgim  23952  recosf1o  24029  resinf1o  24030  efif1olem4  24039  eff1olem  24042  relogcl  24070  eflog  24071  logef  24076  logeftb  24078  logltb  24094  logcn  24137  advlog  24144  advlogexp  24145  logtayl  24150  logccv  24153  dvcxp1  24225  dvcncxp1  24228  cxpcn  24230  loglesqrt  24243  asinrebnd  24372  dvatan  24406  leibpi  24413  efrlim  24440  jensen  24459  amgmlem  24460  lgamgulmlem2  24500  lgamcvg2  24525  wilthlem3  24540  ftalem3  24545  dvdsmulf1o  24664  fsumdvdsmul  24665  dchrelbas2  24706  dchrabs  24729  sum2dchr  24743  dchrisumlem1  24922  logdivsum  24966  log2sumbnd  24977  ostth2  25070  ostth  25072  redwlk  25929  eupares  26295  sspnval  26769  hhssnv  27298  hhssmetdval  27312  foresf1o  28520  ofresid  28617  1stpreimas  28659  xpinpreima  29073  xpinpreima2  29074  cnre2csqlem  29077  rmulccn  29095  zzsnm  29126  cnzh  29135  rezh  29136  measres  29405  cntmeas  29409  cntnevol  29411  1stmbfm  29442  2ndmbfm  29443  carsggect  29500  omsmeas  29505  eulerpartgbij  29554  eulerpartlemgvv  29558  eulerpartlemgs2  29562  iwrdsplit  29569  fibp1  29583  coinfliplem  29660  coinflipprob  29661  gsumnunsn  29735  plyrecld  29745  signstres  29771  bnj1379  29948  bnj1253  30132  bnj1280  30135  subfacp1lem3  30211  subfacp1lem5  30213  erdszelem8  30227  txsconlem  30269  cvmfolem  30308  cvmliftmolem1  30310  cvmliftlem6  30319  cvmliftlem7  30320  cvmliftlem9  30322  mrsubff1  30458  msubff1  30500  fvresval  30704  dfrdg2  30738  frrlem4  30820  sltres  30854  nodense  30881  funpartfv  31015  filnetlem4  31339  icoreunrn  32166  finixpnum  32347  poimirlem3  32365  poimirlem4  32366  poimirlem8  32370  poimirlem26  32388  poimirlem27  32389  itg2gt0cn  32418  areacirclem2  32454  areacirclem4  32456  eqfnun  32469  sdclem2  32491  caures  32509  ismtyres  32560  diaintclN  35148  dibintclN  35257  dihintcl  35434  imaiinfv  36057  mzpcompact2lem  36115  2rexfrabdioph  36161  3rexfrabdioph  36162  4rexfrabdioph  36163  6rexfrabdioph  36164  7rexfrabdioph  36165  jm2.27dlem1  36377  fnwe2lem2  36422  fnwe2lem3  36423  aomclem6  36430  deg1mhm  36587  hausgraph  36592  radcnvrat  37318  wessf1ornlem  38149  mccllem  38447  limcperiod  38478  limcleqr  38494  limclner  38501  resincncf  38543  cncfperiod  38547  icccncfext  38556  cncfiooicclem1  38562  dvbdfbdioolem1  38601  dvnprodlem1  38619  dvnprodlem2  38620  itgioocnicc  38652  stoweidlem28  38704  fourierdlem18  38801  fourierdlem40  38823  fourierdlem42  38825  fourierdlem46  38828  fourierdlem51  38833  fourierdlem70  38852  fourierdlem71  38853  fourierdlem73  38855  fourierdlem74  38856  fourierdlem75  38857  fourierdlem76  38858  fourierdlem78  38860  fourierdlem80  38862  fourierdlem81  38863  fourierdlem82  38864  fourierdlem84  38866  fourierdlem89  38871  fourierdlem90  38872  fourierdlem91  38873  fourierdlem92  38874  fourierdlem93  38875  fourierdlem94  38876  fourierdlem101  38883  fourierdlem103  38885  fourierdlem104  38886  fourierdlem111  38893  fourierdlem112  38894  fourierdlem113  38895  sge0tsms  39056  sge0f1o  39058  sge0sup  39067  sge0less  39068  sge0ltfirp  39076  sge0resrnlem  39079  sge0resplit  39082  sge0le  39083  sge0split  39085  sge0fodjrnlem  39092  sge0iun  39095  meadjun  39138  meadjiunlem  39141  psmeasurelem  39146  caratheodory  39201  hoidmvlelem2  39269  hoidmvlelem3  39270  hoidmvlelem4  39271  voncmpl  39294  mblvon  39312  afvres  39685  iccpartres  39740  iccelpart  39755  pfxccat1  40057  uhgrspansubgrlem  40495  1wlkres  40860  red1wlk  40862  pthdivtx  40916  pthdlem1  40953  resmgmhm  41569  rhmsubclem2  41860  rhmsubcALTVlem2  41879  lincdifsn  41988  lindslinindimp2lem4  42025  lindslinindsimp2lem5  42026  lincresunit3lem2  42044  fdivmpt  42113  amgmwlem  42299
  Copyright terms: Public domain W3C validator