Theorem fvres 5397

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 2658	. . . . 5 |- x e. _V
2	1	brres 4781	. . . 4 |- ( A ( F |` B ) x <-> ( A F x /\ A e. B ) )
3	2	rbaib 887	. . 3 |- ( A e. B -> ( A ( F |` B ) x <-> A F x ) )
4	3	iotabidv 5065	. 2 |- ( A e. B -> ( iota x A ( F |` B ) x ) = ( iota x A F x ) )
5		df-fv 5087	. 2 |- ( ( F |` B ) ` A ) = ( iota x A ( F |` B ) x )
6		df-fv 5087	. 2 |- ( F ` A ) = ( iota x A F x )
7	4, 5, 6	3eqtr4g 2170	1 |- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )

Syntax hints:   -> wi 4   = wceq 1312   e. wcel 1461   class class class wbr 3893   |` cres 4499   iotacio 5042   ` cfv 5079

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-opab 3948  df-xp 4503  df-res 4509  df-iota 5044  df-fv 5087

This theorem is referenced by:  fvresd  5398  funssfv  5399  feqresmpt  5427  fvreseq  5476  respreima  5500  ffvresb  5535  fnressn  5558  fressnfv  5559  fvresi  5565  fvunsng  5566  fvsnun1  5569  fvsnun2  5570  fsnunfv  5573  funfvima  5601  isoresbr  5662  isores3  5668  isoini2  5672  ovres  5862  ofres  5948  offres  5985  fo1stresm  6011  fo2ndresm  6012  fo2ndf  6076  f1o2ndf1  6077  smores  6141  smores2  6143  tfrlem1  6157  rdgival  6231  frec0g  6246  freccllem  6251  frecsuclem  6255  frecrdg  6257  resixp  6579  djulclr  6884  djurclr  6885  djur  6904  updjudhcoinlf  6915  updjudhcoinrg  6916  updjud  6917  finomni  6960  exmidfodomrlemrALT  7004  addpiord  7066  mulpiord  7067  fseq1p1m1  9761  seq3feq2  10130  seq3coll  10472  shftidt  10492  climres  10958  fisumss  11047  isumclim3  11078  fsum2dlemstep  11089  reeff1  11252  eucalgcvga  11579  eucalg  11580  strslfv2d  11838  setsslid  11846  setsslnid  11847  cnptopresti  12243  cnptoprest  12244  lmres  12253  tx1cn  12274  tx2cn  12275  cnmpt1st  12293  cnmpt2nd  12294  remetdval  12519  rescncf  12548  limcdifap  12581  limcresi  12585  djucllem  12690  isomninnlem  12906