Theorem fvres 5602

Description: The value of a restricted function. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fvres	|- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )

Proof of Theorem fvres

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2775	. . . . 5 |- x e. _V
2	1	brres 4966	. . . 4 |- ( A ( F |` B ) x <-> ( A F x /\ A e. B ) )
3	2	rbaib 923	. . 3 |- ( A e. B -> ( A ( F |` B ) x <-> A F x ) )
4	3	iotabidv 5255	. 2 |- ( A e. B -> ( iota x A ( F |` B ) x ) = ( iota x A F x ) )
5		df-fv 5280	. 2 |- ( ( F |` B ) ` A ) = ( iota x A ( F |` B ) x )
6		df-fv 5280	. 2 |- ( F ` A ) = ( iota x A F x )
7	4, 5, 6	3eqtr4g 2263	1 |- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176   class class class wbr 4045   |` cres 4678   iotacio 5231   ` cfv 5272

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-opab 4107  df-xp 4682  df-res 4688  df-iota 5233  df-fv 5280

This theorem is referenced by:  fvresd  5603  funssfv  5604  feqresmpt  5635  fvreseq  5685  respreima  5710  ffvresb  5745  fnressn  5772  fressnfv  5773  fvresi  5779  fvunsng  5780  fvsnun1  5783  fvsnun2  5784  fsnunfv  5787  funfvima  5818  isoresbr  5880  isores3  5886  isoini2  5890  ovres  6088  ofres  6175  offres  6222  fo1stresm  6249  fo2ndresm  6250  fo2ndf  6315  f1o2ndf1  6316  smores  6380  smores2  6382  tfrlem1  6396  rdgival  6470  frec0g  6485  freccllem  6490  frecsuclem  6494  frecrdg  6496  resixp  6822  djulclr  7153  djurclr  7154  djur  7173  updjudhcoinlf  7184  updjudhcoinrg  7185  updjud  7186  finomni  7244  exmidfodomrlemrALT  7313  addpiord  7431  mulpiord  7432  suplocexprlemell  7828  fseq1p1m1  10218  seq3feq2  10623  seqf1oglem2  10667  seq3coll  10989  pfxccat1  11156  shftidt  11177  climres  11647  fisumss  11736  isumclim3  11767  fsum2dlemstep  11778  fprodssdc  11934  fprod2dlemstep  11966  reeff1  12044  eucalgcvga  12413  eucalg  12414  strslfv2d  12908  setsslid  12916  setsslnid  12917  resmhm  13352  resghm  13629  rngmgpf  13732  mgpf  13806  znf1o  14446  cnptopresti  14743  cnptoprest  14744  lmres  14753  tx1cn  14774  tx2cn  14775  cnmpt1st  14793  cnmpt2nd  14794  remetdval  15052  rescncf  15086  limcdifap  15167  limcresi  15171  plyreres  15269  reeff1o  15278  reefiso  15282  ioocosf1o  15359  relogcl  15367  relogef  15369  logltb  15379  mpodvdsmulf1o  15495  fsumdvdsmul  15496  djucllem  15773  012of  15967  2o01f  15968