Theorem nffn

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

	Ref	Expression
Hypotheses	nffn.1	⊢ Ⅎ 𝑥 𝐹
	nffn.2	⊢ Ⅎ 𝑥 𝐴
Assertion	nffn	⊢ Ⅎ 𝑥 𝐹 Fn 𝐴

Proof

Step	Hyp	Ref	Expression
1		nffn.1	⊢ Ⅎ 𝑥 𝐹
2		nffn.2	⊢ Ⅎ 𝑥 𝐴
3		df-fn	⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
4	1	nffun	⊢ Ⅎ 𝑥 Fun 𝐹
5	1	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
6	5 2	nfeq	⊢ Ⅎ 𝑥 dom 𝐹 = 𝐴
7	4 6	nfan	⊢ Ⅎ 𝑥 ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 )
8	3 7	nfxfr	⊢ Ⅎ 𝑥 𝐹 Fn 𝐴