Theorem nffn

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

	Ref	Expression
Hypotheses	nffn.1	|- F/_ x F
	nffn.2	|- F/_ x A
Assertion	nffn	|- F/ x F Fn A

Proof

Step	Hyp	Ref	Expression
1		nffn.1	|- F/_ x F
2		nffn.2	|- F/_ x A
3		df-fn	|- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4	1	nffun	|- F/ x Fun F
5	1	nfdm	|- F/_ x dom F
6	5 2	nfeq	|- F/ x dom F = A
7	4 6	nfan	|- F/ x ( Fun F /\ dom F = A )
8	3 7	nfxfr	|- F/ x F Fn A