Theorem fvres 5696

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 2818	. . . . 5 |- x e. _V
2	1	brres 5046	. . . 4 |- ( A ( F |` B ) x <-> ( A F x /\ A e. B ) )
3	2	rbaib 929	. . 3 |- ( A e. B -> ( A ( F |` B ) x <-> A F x ) )
4	3	iotabidv 5337	. 2 |- ( A e. B -> ( iota x A ( F |` B ) x ) = ( iota x A F x ) )
5		df-fv 5362	. 2 |- ( ( F |` B ) ` A ) = ( iota x A ( F |` B ) x )
6		df-fv 5362	. 2 |- ( F ` A ) = ( iota x A F x )
7	4, 5, 6	3eqtr4g 2292	1 |- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205   class class class wbr 4111   |` cres 4753   iotacio 5312   ` cfv 5354

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-opab 4174  df-xp 4757  df-res 4763  df-iota 5314  df-fv 5362

This theorem is referenced by:  fvresd  5697  funssfv  5698  feqresmpt  5733  fvreseq  5783  respreima  5807  ffvresb  5842  fnressn  5872  fressnfv  5873  fvresi  5879  fvunsng  5880  fvsnun1  5883  fvsnun2  5884  fsnunfv  5887  funfvima  5920  isoresbr  5984  isores3  5990  isoini2  5994  ovres  6196  ofres  6283  offres  6330  fo1stresm  6357  fo2ndresm  6358  fo2ndf  6425  f1o2ndf1  6426  smores  6525  smores2  6527  tfrlem1  6541  rdgival  6615  frec0g  6630  freccllem  6635  frecsuclem  6639  frecrdg  6641  resixp  6970  djulclr  7342  djurclr  7343  djur  7362  updjudhcoinlf  7373  updjudhcoinrg  7374  updjud  7375  finomni  7433  exmidfodomrlemrALT  7508  addpiord  7633  mulpiord  7634  suplocexprlemell  8030  fseq1p1m1  10432  seq3feq2  10842  seqf1oglem2  10886  seq3coll  11218  pfxccat1  11398  shftidt  11522  climres  11992  fisumss  12082  isumclim3  12113  fsum2dlemstep  12124  fprodssdc  12280  fprod2dlemstep  12312  reeff1  12390  eucalgcvga  12759  eucalg  12760  strslfv2d  13272  setsslid  13280  setsslnid  13281  resmhm  13717  resghm  13994  rngmgpf  14098  mgpf  14172  znf1o  14816  cnptopresti  15120  cnptoprest  15121  lmres  15130  tx1cn  15151  tx2cn  15152  cnmpt1st  15170  cnmpt2nd  15171  remetdval  15429  rescncf  15463  limcdifap  15544  limcresi  15548  plyreres  15646  reeff1o  15655  reefiso  15659  ioocosf1o  15736  relogcl  15744  relogef  15746  logltb  15756  mpodvdsmulf1o  15875  fsumdvdsmul  15876  djucllem  16589  012of  16784  2o01f  16785