Metamath Proof Explorer

Theorem fnssresb

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007)

Ref Expression
Assertion fnssresb 
|- ( F Fn A -> ( ( F |` B ) Fn B <-> B C_ A ) )

Proof

Step Hyp Ref Expression
1 df-fn 
 |-  ( ( F |` B ) Fn B <-> ( Fun ( F |` B ) /\ dom ( F |` B ) = B ) )
2 fnfun 
 |-  ( F Fn A -> Fun F )
3 funres 
 |-  ( Fun F -> Fun ( F |` B ) )
4 2 3 syl 
 |-  ( F Fn A -> Fun ( F |` B ) )
5 4 biantrurd 
 |-  ( F Fn A -> ( dom ( F |` B ) = B <-> ( Fun ( F |` B ) /\ dom ( F |` B ) = B ) ) )
6 ssdmres 
 |-  ( B C_ dom F <-> dom ( F |` B ) = B )
7 fndm 
 |-  ( F Fn A -> dom F = A )
8 7 sseq2d 
 |-  ( F Fn A -> ( B C_ dom F <-> B C_ A ) )
9 6 8 bitr3id 
 |-  ( F Fn A -> ( dom ( F |` B ) = B <-> B C_ A ) )
10 5 9 bitr3d 
 |-  ( F Fn A -> ( ( Fun ( F |` B ) /\ dom ( F |` B ) = B ) <-> B C_ A ) )
11 1 10 syl5bb 
 |-  ( F Fn A -> ( ( F |` B ) Fn B <-> B C_ A ) )