Theorem fvres 5650

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 2802	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 5010	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 926	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5300	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5325	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5325	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2287	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200   class class class wbr 4082   ↾ cres 4720  ℩cio 5275  ‘cfv 5317

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-opab 4145  df-xp 4724  df-res 4730  df-iota 5277  df-fv 5325

This theorem is referenced by:  fvresd  5651  funssfv  5652  feqresmpt  5687  fvreseq  5737  respreima  5762  ffvresb  5797  fnressn  5824  fressnfv  5825  fvresi  5831  fvunsng  5832  fvsnun1  5835  fvsnun2  5836  fsnunfv  5839  funfvima  5870  isoresbr  5932  isores3  5938  isoini2  5942  ovres  6144  ofres  6231  offres  6278  fo1stresm  6305  fo2ndresm  6306  fo2ndf  6371  f1o2ndf1  6372  smores  6436  smores2  6438  tfrlem1  6452  rdgival  6526  frec0g  6541  freccllem  6546  frecsuclem  6550  frecrdg  6552  resixp  6878  djulclr  7212  djurclr  7213  djur  7232  updjudhcoinlf  7243  updjudhcoinrg  7244  updjud  7245  finomni  7303  exmidfodomrlemrALT  7377  addpiord  7499  mulpiord  7500  suplocexprlemell  7896  fseq1p1m1  10286  seq3feq2  10693  seqf1oglem2  10737  seq3coll  11059  pfxccat1  11229  shftidt  11339  climres  11809  fisumss  11898  isumclim3  11929  fsum2dlemstep  11940  fprodssdc  12096  fprod2dlemstep  12128  reeff1  12206  eucalgcvga  12575  eucalg  12576  strslfv2d  13070  setsslid  13078  setsslnid  13079  resmhm  13515  resghm  13792  rngmgpf  13895  mgpf  13969  znf1o  14609  cnptopresti  14906  cnptoprest  14907  lmres  14916  tx1cn  14937  tx2cn  14938  cnmpt1st  14956  cnmpt2nd  14957  remetdval  15215  rescncf  15249  limcdifap  15330  limcresi  15334  plyreres  15432  reeff1o  15441  reefiso  15445  ioocosf1o  15522  relogcl  15530  relogef  15532  logltb  15542  mpodvdsmulf1o  15658  fsumdvdsmul  15659  djucllem  16122  012of  16316  2o01f  16317