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  5839  fressnfv  5840  fvresi  5846  fvunsng  5847  fvsnun1  5850  fvsnun2  5851  fsnunfv  5854  funfvima  5885  isoresbr  5949  isores3  5955  isoini2  5959  ovres  6161  ofres  6249  offres  6296  fo1stresm  6323  fo2ndresm  6324  fo2ndf  6391  f1o2ndf1  6392  smores  6457  smores2  6459  tfrlem1  6473  rdgival  6547  frec0g  6562  freccllem  6567  frecsuclem  6571  frecrdg  6573  resixp  6901  djulclr  7247  djurclr  7248  djur  7267  updjudhcoinlf  7278  updjudhcoinrg  7279  updjud  7280  finomni  7338  exmidfodomrlemrALT  7413  addpiord  7535  mulpiord  7536  suplocexprlemell  7932  fseq1p1m1  10328  seq3feq2  10737  seqf1oglem2  10781  seq3coll  11105  pfxccat1  11282  shftidt  11393  climres  11863  fisumss  11952  isumclim3  11983  fsum2dlemstep  11994  fprodssdc  12150  fprod2dlemstep  12182  reeff1  12260  eucalgcvga  12629  eucalg  12630  strslfv2d  13124  setsslid  13132  setsslnid  13133  resmhm  13569  resghm  13846  rngmgpf  13949  mgpf  14023  znf1o  14664  cnptopresti  14961  cnptoprest  14962  lmres  14971  tx1cn  14992  tx2cn  14993  cnmpt1st  15011  cnmpt2nd  15012  remetdval  15270  rescncf  15304  limcdifap  15385  limcresi  15389  plyreres  15487  reeff1o  15496  reefiso  15500  ioocosf1o  15577  relogcl  15585  relogef  15587  logltb  15597  mpodvdsmulf1o  15713  fsumdvdsmul  15714  djucllem  16396  012of  16592  2o01f  16593