Metamath Proof Explorer


Theorem nffn

Description: Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004)

Ref Expression
Hypotheses nffn.1 _xF
nffn.2 _xA
Assertion nffn xFFnA

Proof

Step Hyp Ref Expression
1 nffn.1 _xF
2 nffn.2 _xA
3 df-fn FFnAFunFdomF=A
4 1 nffun xFunF
5 1 nfdm _xdomF
6 5 2 nfeq xdomF=A
7 4 6 nfan xFunFdomF=A
8 3 7 nfxfr xFFnA