Metamath Proof Explorer

Theorem fnresin2

Description: Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994)

Ref Expression
Assertion fnresin2 
|- ( F Fn A -> ( F |` ( B i^i A ) ) Fn ( B i^i A ) )

Proof

Step Hyp Ref Expression
1 inss2 
 |-  ( B i^i A ) C_ A
2 fnssres 
 |-  ( ( F Fn A /\ ( B i^i A ) C_ A ) -> ( F |` ( B i^i A ) ) Fn ( B i^i A ) )
3 1 2 mpan2 
 |-  ( F Fn A -> ( F |` ( B i^i A ) ) Fn ( B i^i A ) )