Theorem fnssres 3600

Description: Restriction of a function with a subclass of its domain.

Assertion

Ref	Expression
fnssres	|- ((F Fn A /\ B (_ A) -> (F |` B) Fn B)

Proof of Theorem fnssres

Step	Hyp	Ref	Expression
1		fnssresb 3599	. 2 |- (F Fn A -> ((F |` B) Fn B <-> B (_ A))
2	1	biimpar 417	1 |- ((F Fn A /\ B (_ A) -> (F |` B) Fn B)

Syntax hints:   -> wi 3   /\ wa 223   (_ wss 2047   |` cres 3172   Fn wfn 3177

This theorem is referenced by:  fnresin1 3601  fnresin2 3602  fssres 3643  fvreseq 3799  fnressn 3837  tz7.48lem 3955  tz7.49c 3960  df1st2 4126  df2nd2 4127  mulnzcnopr 5702  shftres 6344  seqzfn 6539  seq0fn 6546  seq1ublem 6911  seq1ub 6912  ghgrpilem4 8136  sspg 8387  ssps 8389  sspmlem 8391  sspn 8395  efghgrpilem 8719  hhssnv 9134

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620  df-opab 2667  df-id 2835  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-res 3190  df-fun 3192  df-fn 3193

Copyright terms: Public domain