Theorem fvres 5599

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 2774	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 4964	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 922	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5253	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5278	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5278	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2262	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1372   ∈ wcel 2175   class class class wbr 4043   ↾ cres 4676  ℩cio 5229  ‘cfv 5270

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-xp 4680  df-res 4686  df-iota 5231  df-fv 5278

This theorem is referenced by:  fvresd  5600  funssfv  5601  feqresmpt  5632  fvreseq  5682  respreima  5707  ffvresb  5742  fnressn  5769  fressnfv  5770  fvresi  5776  fvunsng  5777  fvsnun1  5780  fvsnun2  5781  fsnunfv  5784  funfvima  5815  isoresbr  5877  isores3  5883  isoini2  5887  ovres  6085  ofres  6172  offres  6219  fo1stresm  6246  fo2ndresm  6247  fo2ndf  6312  f1o2ndf1  6313  smores  6377  smores2  6379  tfrlem1  6393  rdgival  6467  frec0g  6482  freccllem  6487  frecsuclem  6491  frecrdg  6493  resixp  6819  djulclr  7150  djurclr  7151  djur  7170  updjudhcoinlf  7181  updjudhcoinrg  7182  updjud  7183  finomni  7241  exmidfodomrlemrALT  7310  addpiord  7428  mulpiord  7429  suplocexprlemell  7825  fseq1p1m1  10215  seq3feq2  10619  seqf1oglem2  10663  seq3coll  10985  shftidt  11115  climres  11585  fisumss  11674  isumclim3  11705  fsum2dlemstep  11716  fprodssdc  11872  fprod2dlemstep  11904  reeff1  11982  eucalgcvga  12351  eucalg  12352  strslfv2d  12846  setsslid  12854  setsslnid  12855  resmhm  13290  resghm  13567  rngmgpf  13670  mgpf  13744  znf1o  14384  cnptopresti  14681  cnptoprest  14682  lmres  14691  tx1cn  14712  tx2cn  14713  cnmpt1st  14731  cnmpt2nd  14732  remetdval  14990  rescncf  15024  limcdifap  15105  limcresi  15109  plyreres  15207  reeff1o  15216  reefiso  15220  ioocosf1o  15297  relogcl  15305  relogef  15307  logltb  15317  mpodvdsmulf1o  15433  fsumdvdsmul  15434  djucllem  15698  012of  15892  2o01f  15893