Theorem fvres 5313

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 2622	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 4707	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 868	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 4988	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5010	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5010	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2145	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1289   ∈ wcel 1438   class class class wbr 3837   ↾ cres 4430  ℩cio 4965  ‘cfv 5002

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027

This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-xp 4434  df-res 4440  df-iota 4967  df-fv 5010

This theorem is referenced by:  funssfv  5314  feqresmpt  5342  fvreseq  5387  respreima  5411  ffvresb  5445  fnressn  5467  fressnfv  5468  fvresi  5474  fvunsng  5475  fvsnun1  5478  fvsnun2  5479  fsnunfv  5481  funfvima  5508  isoresbr  5570  isores3  5576  isoini2  5580  ovres  5766  ofres  5851  offres  5888  fo1stresm  5914  fo2ndresm  5915  fo2ndf  5974  f1o2ndf1  5975  smores  6039  smores2  6041  tfrlem1  6055  rdgival  6129  frec0g  6144  freccllem  6149  frecsuclem  6153  frecrdg  6155  djulclr  6720  djurclr  6721  updjudhcoinlf  6750  updjudhcoinrg  6751  updjud  6752  finomni  6775  exmidfodomrlemrALT  6808  addpiord  6854  mulpiord  6855  fseq1p1m1  9475  iseqfeq2  9856  seq3feq2  9858  iseqcoll  10212  shftidt  10232  climres  10655  fisumss  10748  isumclim3  10780  fsum2dlemstep  10791  eucialgcvga  11133  eucialg  11134  djucllem  11357