Metamath Proof Explorer

Theorem fnresin1

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

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

Proof

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