Theorem fvres 5659

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.

Step	Hyp	Ref	Expression
1		vex 2803	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 5017	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 926	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5307	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5332	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5332	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2287	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200   class class class wbr 4086   ↾ cres 4725  ℩cio 5282  ‘cfv 5324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-xp 4729  df-res 4735  df-iota 5284  df-fv 5332

This theorem is referenced by:  fvresd  5660  funssfv  5661  feqresmpt  5696  fvreseq  5746  respreima  5771  ffvresb  5806  fnressn  5835  fressnfv  5836  fvresi  5842  fvunsng  5843  fvsnun1  5846  fvsnun2  5847  fsnunfv  5850  funfvima  5881  isoresbr  5945  isores3  5951  isoini2  5955  ovres  6157  ofres  6245  offres  6292  fo1stresm  6319  fo2ndresm  6320  fo2ndf  6387  f1o2ndf1  6388  smores  6453  smores2  6455  tfrlem1  6469  rdgival  6543  frec0g  6558  freccllem  6563  frecsuclem  6567  frecrdg  6569  resixp  6897  djulclr  7239  djurclr  7240  djur  7259  updjudhcoinlf  7270  updjudhcoinrg  7271  updjud  7272  finomni  7330  exmidfodomrlemrALT  7404  addpiord  7526  mulpiord  7527  suplocexprlemell  7923  fseq1p1m1  10319  seq3feq2  10728  seqf1oglem2  10772  seq3coll  11096  pfxccat1  11273  shftidt  11384  climres  11854  fisumss  11943  isumclim3  11974  fsum2dlemstep  11985  fprodssdc  12141  fprod2dlemstep  12173  reeff1  12251  eucalgcvga  12620  eucalg  12621  strslfv2d  13115  setsslid  13123  setsslnid  13124  resmhm  13560  resghm  13837  rngmgpf  13940  mgpf  14014  znf1o  14655  cnptopresti  14952  cnptoprest  14953  lmres  14962  tx1cn  14983  tx2cn  14984  cnmpt1st  15002  cnmpt2nd  15003  remetdval  15261  rescncf  15295  limcdifap  15376  limcresi  15380  plyreres  15478  reeff1o  15487  reefiso  15491  ioocosf1o  15568  relogcl  15576  relogef  15578  logltb  15588  mpodvdsmulf1o  15704  fsumdvdsmul  15705  djucllem  16332  012of  16528  2o01f  16529