Metamath Proof Explorer


Theorem nffun

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

Ref Expression
Hypothesis nffun.1 _xF
Assertion nffun xFunF

Proof

Step Hyp Ref Expression
1 nffun.1 _xF
2 df-fun FunFRelFFF-1I
3 1 nfrel xRelF
4 1 nfcnv _xF-1
5 1 4 nfco _xFF-1
6 nfcv _xI
7 5 6 nfss xFF-1I
8 3 7 nfan xRelFFF-1I
9 2 8 nfxfr xFunF