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 FFnAFABFnAB

Proof

Step Hyp Ref Expression
1 inss1 ABA
2 fnssres FFnAABAFABFnAB
3 1 2 mpan2 FFnAFABFnAB