Theorem fvres 5579

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 2763	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 4949	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 922	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5238	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5263	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5263	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2251	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164   class class class wbr 4030   ↾ cres 4662  ℩cio 5214  ‘cfv 5255

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-opab 4092  df-xp 4666  df-res 4672  df-iota 5216  df-fv 5263

This theorem is referenced by:  fvresd  5580  funssfv  5581  feqresmpt  5612  fvreseq  5662  respreima  5687  ffvresb  5722  fnressn  5745  fressnfv  5746  fvresi  5752  fvunsng  5753  fvsnun1  5756  fvsnun2  5757  fsnunfv  5760  funfvima  5791  isoresbr  5853  isores3  5859  isoini2  5863  ovres  6060  ofres  6147  offres  6189  fo1stresm  6216  fo2ndresm  6217  fo2ndf  6282  f1o2ndf1  6283  smores  6347  smores2  6349  tfrlem1  6363  rdgival  6437  frec0g  6452  freccllem  6457  frecsuclem  6461  frecrdg  6463  resixp  6789  djulclr  7110  djurclr  7111  djur  7130  updjudhcoinlf  7141  updjudhcoinrg  7142  updjud  7143  finomni  7201  exmidfodomrlemrALT  7265  addpiord  7378  mulpiord  7379  suplocexprlemell  7775  fseq1p1m1  10163  seq3feq2  10550  seqf1oglem2  10594  seq3coll  10916  shftidt  10980  climres  11449  fisumss  11538  isumclim3  11569  fsum2dlemstep  11580  fprodssdc  11736  fprod2dlemstep  11768  reeff1  11846  eucalgcvga  12199  eucalg  12200  strslfv2d  12664  setsslid  12672  setsslnid  12673  resmhm  13062  resghm  13333  rngmgpf  13436  mgpf  13510  znf1o  14150  cnptopresti  14417  cnptoprest  14418  lmres  14427  tx1cn  14448  tx2cn  14449  cnmpt1st  14467  cnmpt2nd  14468  remetdval  14726  rescncf  14760  limcdifap  14841  limcresi  14845  plyreres  14942  reeff1o  14949  reefiso  14953  ioocosf1o  15030  relogcl  15038  relogef  15040  logltb  15050  djucllem  15362  012of  15556  2o01f  15557