Theorem fvres 5594

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 2774	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 4962	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 922	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5251	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5276	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5276	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2262	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1372   ∈ wcel 2175   class class class wbr 4043   ↾ cres 4675  ℩cio 5227  ‘cfv 5268

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-xp 4679  df-res 4685  df-iota 5229  df-fv 5276

This theorem is referenced by:  fvresd  5595  funssfv  5596  feqresmpt  5627  fvreseq  5677  respreima  5702  ffvresb  5737  fnressn  5760  fressnfv  5761  fvresi  5767  fvunsng  5768  fvsnun1  5771  fvsnun2  5772  fsnunfv  5775  funfvima  5806  isoresbr  5868  isores3  5874  isoini2  5878  ovres  6076  ofres  6163  offres  6210  fo1stresm  6237  fo2ndresm  6238  fo2ndf  6303  f1o2ndf1  6304  smores  6368  smores2  6370  tfrlem1  6384  rdgival  6458  frec0g  6473  freccllem  6478  frecsuclem  6482  frecrdg  6484  resixp  6810  djulclr  7133  djurclr  7134  djur  7153  updjudhcoinlf  7164  updjudhcoinrg  7165  updjud  7166  finomni  7224  exmidfodomrlemrALT  7293  addpiord  7411  mulpiord  7412  suplocexprlemell  7808  fseq1p1m1  10198  seq3feq2  10602  seqf1oglem2  10646  seq3coll  10968  shftidt  11063  climres  11533  fisumss  11622  isumclim3  11653  fsum2dlemstep  11664  fprodssdc  11820  fprod2dlemstep  11852  reeff1  11930  eucalgcvga  12299  eucalg  12300  strslfv2d  12794  setsslid  12802  setsslnid  12803  resmhm  13237  resghm  13514  rngmgpf  13617  mgpf  13691  znf1o  14331  cnptopresti  14628  cnptoprest  14629  lmres  14638  tx1cn  14659  tx2cn  14660  cnmpt1st  14678  cnmpt2nd  14679  remetdval  14937  rescncf  14971  limcdifap  15052  limcresi  15056  plyreres  15154  reeff1o  15163  reefiso  15167  ioocosf1o  15244  relogcl  15252  relogef  15254  logltb  15264  mpodvdsmulf1o  15380  fsumdvdsmul  15381  djucllem  15600  012of  15794  2o01f  15795