Theorem fvres 5663

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 2805	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 5019	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 928	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5309	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5334	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5334	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2289	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202   class class class wbr 4088   ↾ cres 4727  ℩cio 5284  ‘cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-xp 4731  df-res 4737  df-iota 5286  df-fv 5334

This theorem is referenced by:  fvresd  5664  funssfv  5665  feqresmpt  5700  fvreseq  5750  respreima  5775  ffvresb  5810  fnressn  5840  fressnfv  5841  fvresi  5847  fvunsng  5848  fvsnun1  5851  fvsnun2  5852  fsnunfv  5855  funfvima  5886  isoresbr  5950  isores3  5956  isoini2  5960  ovres  6162  ofres  6250  offres  6297  fo1stresm  6324  fo2ndresm  6325  fo2ndf  6392  f1o2ndf1  6393  smores  6458  smores2  6460  tfrlem1  6474  rdgival  6548  frec0g  6563  freccllem  6568  frecsuclem  6572  frecrdg  6574  resixp  6902  djulclr  7248  djurclr  7249  djur  7268  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  finomni  7339  exmidfodomrlemrALT  7414  addpiord  7536  mulpiord  7537  suplocexprlemell  7933  fseq1p1m1  10329  seq3feq2  10739  seqf1oglem2  10783  seq3coll  11107  pfxccat1  11287  shftidt  11398  climres  11868  fisumss  11958  isumclim3  11989  fsum2dlemstep  12000  fprodssdc  12156  fprod2dlemstep  12188  reeff1  12266  eucalgcvga  12635  eucalg  12636  strslfv2d  13130  setsslid  13138  setsslnid  13139  resmhm  13575  resghm  13852  rngmgpf  13956  mgpf  14030  znf1o  14671  cnptopresti  14968  cnptoprest  14969  lmres  14978  tx1cn  14999  tx2cn  15000  cnmpt1st  15018  cnmpt2nd  15019  remetdval  15277  rescncf  15311  limcdifap  15392  limcresi  15396  plyreres  15494  reeff1o  15503  reefiso  15507  ioocosf1o  15584  relogcl  15592  relogef  15594  logltb  15604  mpodvdsmulf1o  15720  fsumdvdsmul  15721  djucllem  16422  012of  16618  2o01f  16619