Theorem fvres 5578

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 2763	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 4948	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 922	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5237	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5262	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5262	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2251	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164   class class class wbr 4029   ↾ cres 4661  ℩cio 5213  ‘cfv 5254

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-xp 4665  df-res 4671  df-iota 5215  df-fv 5262

This theorem is referenced by:  fvresd  5579  funssfv  5580  feqresmpt  5611  fvreseq  5661  respreima  5686  ffvresb  5721  fnressn  5744  fressnfv  5745  fvresi  5751  fvunsng  5752  fvsnun1  5755  fvsnun2  5756  fsnunfv  5759  funfvima  5790  isoresbr  5852  isores3  5858  isoini2  5862  ovres  6058  ofres  6145  offres  6187  fo1stresm  6214  fo2ndresm  6215  fo2ndf  6280  f1o2ndf1  6281  smores  6345  smores2  6347  tfrlem1  6361  rdgival  6435  frec0g  6450  freccllem  6455  frecsuclem  6459  frecrdg  6461  resixp  6787  djulclr  7108  djurclr  7109  djur  7128  updjudhcoinlf  7139  updjudhcoinrg  7140  updjud  7141  finomni  7199  exmidfodomrlemrALT  7263  addpiord  7376  mulpiord  7377  suplocexprlemell  7773  fseq1p1m1  10160  seq3feq2  10547  seqf1oglem2  10591  seq3coll  10913  shftidt  10977  climres  11446  fisumss  11535  isumclim3  11566  fsum2dlemstep  11577  fprodssdc  11733  fprod2dlemstep  11765  reeff1  11843  eucalgcvga  12196  eucalg  12197  strslfv2d  12661  setsslid  12669  setsslnid  12670  resmhm  13059  resghm  13330  rngmgpf  13433  mgpf  13507  znf1o  14139  cnptopresti  14406  cnptoprest  14407  lmres  14416  tx1cn  14437  tx2cn  14438  cnmpt1st  14456  cnmpt2nd  14457  remetdval  14707  rescncf  14736  limcdifap  14816  limcresi  14820  reeff1o  14908  reefiso  14912  ioocosf1o  14989  relogcl  14997  relogef  14999  logltb  15009  djucllem  15292  012of  15486  2o01f  15487