Metamath Proof Explorer


Theorem funfni

Description: Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004)

Ref Expression
Hypothesis funfni.1 FunFBdomFφ
Assertion funfni FFnABAφ

Proof

Step Hyp Ref Expression
1 funfni.1 FunFBdomFφ
2 fnfun FFnAFunF
3 fndm FFnAdomF=A
4 3 eleq2d FFnABdomFBA
5 4 biimpar FFnABABdomF
6 2 5 1 syl2an2r FFnABAφ