Theorem fvres 5672

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 2806	. . . . 5 |- x e. _V
2	1	brres 5025	. . . 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 5316	. 2 |- ( A e. B -> ( iota x A ( F |` B ) x ) = ( iota x A F x ) )
5		df-fv 5341	. 2 |- ( ( F |` B ) ` A ) = ( iota x A ( F |` B ) x )
6		df-fv 5341	. 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 1398   e. wcel 2202   class class class wbr 4093   |` cres 4733   iotacio 5291   ` cfv 5333

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 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-xp 4737  df-res 4743  df-iota 5293  df-fv 5341

This theorem is referenced by:  fvresd  5673  funssfv  5674  feqresmpt  5709  fvreseq  5759  respreima  5783  ffvresb  5818  fnressn  5848  fressnfv  5849  fvresi  5855  fvunsng  5856  fvsnun1  5859  fvsnun2  5860  fsnunfv  5863  funfvima  5896  isoresbr  5960  isores3  5966  isoini2  5970  ovres  6172  ofres  6259  offres  6306  fo1stresm  6333  fo2ndresm  6334  fo2ndf  6401  f1o2ndf1  6402  smores  6501  smores2  6503  tfrlem1  6517  rdgival  6591  frec0g  6606  freccllem  6611  frecsuclem  6615  frecrdg  6617  resixp  6945  djulclr  7308  djurclr  7309  djur  7328  updjudhcoinlf  7339  updjudhcoinrg  7340  updjud  7341  finomni  7399  exmidfodomrlemrALT  7474  addpiord  7596  mulpiord  7597  suplocexprlemell  7993  fseq1p1m1  10391  seq3feq2  10801  seqf1oglem2  10845  seq3coll  11169  pfxccat1  11349  shftidt  11473  climres  11943  fisumss  12033  isumclim3  12064  fsum2dlemstep  12075  fprodssdc  12231  fprod2dlemstep  12263  reeff1  12341  eucalgcvga  12710  eucalg  12711  strslfv2d  13205  setsslid  13213  setsslnid  13214  resmhm  13650  resghm  13927  rngmgpf  14031  mgpf  14105  znf1o  14747  cnptopresti  15049  cnptoprest  15050  lmres  15059  tx1cn  15080  tx2cn  15081  cnmpt1st  15099  cnmpt2nd  15100  remetdval  15358  rescncf  15392  limcdifap  15473  limcresi  15477  plyreres  15575  reeff1o  15584  reefiso  15588  ioocosf1o  15665  relogcl  15673  relogef  15675  logltb  15685  mpodvdsmulf1o  15804  fsumdvdsmul  15805  djucllem  16518  012of  16713  2o01f  16714