Theorem fvres 5623

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 2779	. . . . 5 |- x e. _V
2	1	brres 4984	. . . 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 5273	. 2 |- ( A e. B -> ( iota x A ( F |` B ) x ) = ( iota x A F x ) )
5		df-fv 5298	. 2 |- ( ( F |` B ) ` A ) = ( iota x A ( F |` B ) x )
6		df-fv 5298	. 2 |- ( F ` A ) = ( iota x A F x )
7	4, 5, 6	3eqtr4g 2265	1 |- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2178   class class class wbr 4059   |` cres 4695   iotacio 5249   ` cfv 5290

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-opab 4122  df-xp 4699  df-res 4705  df-iota 5251  df-fv 5298

This theorem is referenced by:  fvresd  5624  funssfv  5625  feqresmpt  5656  fvreseq  5706  respreima  5731  ffvresb  5766  fnressn  5793  fressnfv  5794  fvresi  5800  fvunsng  5801  fvsnun1  5804  fvsnun2  5805  fsnunfv  5808  funfvima  5839  isoresbr  5901  isores3  5907  isoini2  5911  ovres  6109  ofres  6196  offres  6243  fo1stresm  6270  fo2ndresm  6271  fo2ndf  6336  f1o2ndf1  6337  smores  6401  smores2  6403  tfrlem1  6417  rdgival  6491  frec0g  6506  freccllem  6511  frecsuclem  6515  frecrdg  6517  resixp  6843  djulclr  7177  djurclr  7178  djur  7197  updjudhcoinlf  7208  updjudhcoinrg  7209  updjud  7210  finomni  7268  exmidfodomrlemrALT  7342  addpiord  7464  mulpiord  7465  suplocexprlemell  7861  fseq1p1m1  10251  seq3feq2  10658  seqf1oglem2  10702  seq3coll  11024  pfxccat1  11193  shftidt  11259  climres  11729  fisumss  11818  isumclim3  11849  fsum2dlemstep  11860  fprodssdc  12016  fprod2dlemstep  12048  reeff1  12126  eucalgcvga  12495  eucalg  12496  strslfv2d  12990  setsslid  12998  setsslnid  12999  resmhm  13434  resghm  13711  rngmgpf  13814  mgpf  13888  znf1o  14528  cnptopresti  14825  cnptoprest  14826  lmres  14835  tx1cn  14856  tx2cn  14857  cnmpt1st  14875  cnmpt2nd  14876  remetdval  15134  rescncf  15168  limcdifap  15249  limcresi  15253  plyreres  15351  reeff1o  15360  reefiso  15364  ioocosf1o  15441  relogcl  15449  relogef  15451  logltb  15461  mpodvdsmulf1o  15577  fsumdvdsmul  15578  djucllem  15936  012of  16130  2o01f  16131