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  11086  climres  11556  fisumss  11645  isumclim3  11676  fsum2dlemstep  11687  fprodssdc  11843  fprod2dlemstep  11875  reeff1  11953  eucalgcvga  12322  eucalg  12323  strslfv2d  12817  setsslid  12825  setsslnid  12826  resmhm  13261  resghm  13538  rngmgpf  13641  mgpf  13715  znf1o  14355  cnptopresti  14652  cnptoprest  14653  lmres  14662  tx1cn  14683  tx2cn  14684  cnmpt1st  14702  cnmpt2nd  14703  remetdval  14961  rescncf  14995  limcdifap  15076  limcresi  15080  plyreres  15178  reeff1o  15187  reefiso  15191  ioocosf1o  15268  relogcl  15276  relogef  15278  logltb  15288  mpodvdsmulf1o  15404  fsumdvdsmul  15405  djucllem  15669  012of  15863  2o01f  15864