Theorem fvres 5663

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 2805	. . . . 5 |- x e. _V
2	1	brres 5019	. . . 4 |- ( A ( F |` B ) x <-> ( A F x /\ A e. B ) )
3	2	rbaib 928	. . 3 |- ( A e. B -> ( A ( F |` B ) x <-> A F x ) )
4	3	iotabidv 5309	. 2 |- ( A e. B -> ( iota x A ( F |` B ) x ) = ( iota x A F x ) )
5		df-fv 5334	. 2 |- ( ( F |` B ) ` A ) = ( iota x A ( F |` B ) x )
6		df-fv 5334	. 2 |- ( F ` A ) = ( iota x A F x )
7	4, 5, 6	3eqtr4g 2289	1 |- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202   class class class wbr 4088   |` cres 4727   iotacio 5284   ` cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-xp 4731  df-res 4737  df-iota 5286  df-fv 5334

This theorem is referenced by:  fvresd  5664  funssfv  5665  feqresmpt  5700  fvreseq  5750  respreima  5775  ffvresb  5810  fnressn  5840  fressnfv  5841  fvresi  5847  fvunsng  5848  fvsnun1  5851  fvsnun2  5852  fsnunfv  5855  funfvima  5886  isoresbr  5950  isores3  5956  isoini2  5960  ovres  6162  ofres  6250  offres  6297  fo1stresm  6324  fo2ndresm  6325  fo2ndf  6392  f1o2ndf1  6393  smores  6458  smores2  6460  tfrlem1  6474  rdgival  6548  frec0g  6563  freccllem  6568  frecsuclem  6572  frecrdg  6574  resixp  6902  djulclr  7248  djurclr  7249  djur  7268  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  finomni  7339  exmidfodomrlemrALT  7414  addpiord  7536  mulpiord  7537  suplocexprlemell  7933  fseq1p1m1  10329  seq3feq2  10739  seqf1oglem2  10783  seq3coll  11107  pfxccat1  11287  shftidt  11411  climres  11881  fisumss  11971  isumclim3  12002  fsum2dlemstep  12013  fprodssdc  12169  fprod2dlemstep  12201  reeff1  12279  eucalgcvga  12648  eucalg  12649  strslfv2d  13143  setsslid  13151  setsslnid  13152  resmhm  13588  resghm  13865  rngmgpf  13969  mgpf  14043  znf1o  14684  cnptopresti  14981  cnptoprest  14982  lmres  14991  tx1cn  15012  tx2cn  15013  cnmpt1st  15031  cnmpt2nd  15032  remetdval  15290  rescncf  15324  limcdifap  15405  limcresi  15409  plyreres  15507  reeff1o  15516  reefiso  15520  ioocosf1o  15597  relogcl  15605  relogef  15607  logltb  15617  mpodvdsmulf1o  15733  fsumdvdsmul  15734  djucllem  16447  012of  16643  2o01f  16644