Theorem fvres 5494

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 2715	. . . . 5 |- x e. _V
2	1	brres 4874	. . . 4 |- ( A ( F |` B ) x <-> ( A F x /\ A e. B ) )
3	2	rbaib 907	. . 3 |- ( A e. B -> ( A ( F |` B ) x <-> A F x ) )
4	3	iotabidv 5158	. 2 |- ( A e. B -> ( iota x A ( F |` B ) x ) = ( iota x A F x ) )
5		df-fv 5180	. 2 |- ( ( F |` B ) ` A ) = ( iota x A ( F |` B ) x )
6		df-fv 5180	. 2 |- ( F ` A ) = ( iota x A F x )
7	4, 5, 6	3eqtr4g 2215	1 |- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )

Syntax hints:   -> wi 4   = wceq 1335   e. wcel 2128   class class class wbr 3967   |` cres 4590   iotacio 5135   ` cfv 5172

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 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4084  ax-pow 4137  ax-pr 4171

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-uni 3775  df-br 3968  df-opab 4028  df-xp 4594  df-res 4600  df-iota 5137  df-fv 5180

This theorem is referenced by:  fvresd  5495  funssfv  5496  feqresmpt  5524  fvreseq  5573  respreima  5597  ffvresb  5632  fnressn  5655  fressnfv  5656  fvresi  5662  fvunsng  5663  fvsnun1  5666  fvsnun2  5667  fsnunfv  5670  funfvima  5700  isoresbr  5761  isores3  5767  isoini2  5771  ovres  5962  ofres  6048  offres  6085  fo1stresm  6111  fo2ndresm  6112  fo2ndf  6176  f1o2ndf1  6177  smores  6241  smores2  6243  tfrlem1  6257  rdgival  6331  frec0g  6346  freccllem  6351  frecsuclem  6355  frecrdg  6357  resixp  6680  djulclr  6995  djurclr  6996  djur  7015  updjudhcoinlf  7026  updjudhcoinrg  7027  updjud  7028  finomni  7085  exmidfodomrlemrALT  7140  addpiord  7238  mulpiord  7239  suplocexprlemell  7635  fseq1p1m1  10002  seq3feq2  10378  seq3coll  10724  shftidt  10744  climres  11211  fisumss  11300  isumclim3  11331  fsum2dlemstep  11342  fprodssdc  11498  fprod2dlemstep  11530  reeff1  11608  eucalgcvga  11950  eucalg  11951  strslfv2d  12302  setsslid  12310  setsslnid  12311  cnptopresti  12708  cnptoprest  12709  lmres  12718  tx1cn  12739  tx2cn  12740  cnmpt1st  12758  cnmpt2nd  12759  remetdval  13009  rescncf  13038  limcdifap  13101  limcresi  13105  reeff1o  13164  reefiso  13168  ioocosf1o  13245  relogcl  13253  relogef  13255  logltb  13265  djucllem  13445  012of  13638  2o01f  13639