Theorem fvres 5520

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 2733	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 4897	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 916	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5181	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5206	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5206	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2228	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141   class class class wbr 3989   ↾ cres 4613  ℩cio 5158  ‘cfv 5198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-opab 4051  df-xp 4617  df-res 4623  df-iota 5160  df-fv 5206

This theorem is referenced by:  fvresd  5521  funssfv  5522  feqresmpt  5550  fvreseq  5599  respreima  5624  ffvresb  5659  fnressn  5682  fressnfv  5683  fvresi  5689  fvunsng  5690  fvsnun1  5693  fvsnun2  5694  fsnunfv  5697  funfvima  5727  isoresbr  5788  isores3  5794  isoini2  5798  ovres  5992  ofres  6075  offres  6114  fo1stresm  6140  fo2ndresm  6141  fo2ndf  6206  f1o2ndf1  6207  smores  6271  smores2  6273  tfrlem1  6287  rdgival  6361  frec0g  6376  freccllem  6381  frecsuclem  6385  frecrdg  6387  resixp  6711  djulclr  7026  djurclr  7027  djur  7046  updjudhcoinlf  7057  updjudhcoinrg  7058  updjud  7059  finomni  7116  exmidfodomrlemrALT  7180  addpiord  7278  mulpiord  7279  suplocexprlemell  7675  fseq1p1m1  10050  seq3feq2  10426  seq3coll  10777  shftidt  10797  climres  11266  fisumss  11355  isumclim3  11386  fsum2dlemstep  11397  fprodssdc  11553  fprod2dlemstep  11585  reeff1  11663  eucalgcvga  12012  eucalg  12013  strslfv2d  12458  setsslid  12466  setsslnid  12467  cnptopresti  13032  cnptoprest  13033  lmres  13042  tx1cn  13063  tx2cn  13064  cnmpt1st  13082  cnmpt2nd  13083  remetdval  13333  rescncf  13362  limcdifap  13425  limcresi  13429  reeff1o  13488  reefiso  13492  ioocosf1o  13569  relogcl  13577  relogef  13579  logltb  13589  djucllem  13835  012of  14028  2o01f  14029