Theorem nffun

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

	Ref	Expression
Hypothesis	nffun.1	⊢ Ⅎ 𝑥 𝐹
Assertion	nffun	⊢ Ⅎ 𝑥 Fun 𝐹

Proof

Step	Hyp	Ref	Expression
1		nffun.1	⊢ Ⅎ 𝑥 𝐹
2		df-fun	⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ) )
3	1	nfrel	⊢ Ⅎ 𝑥 Rel 𝐹
4	1	nfcnv	⊢ Ⅎ 𝑥 ◡ 𝐹
5	1 4	nfco	⊢ Ⅎ 𝑥 ( 𝐹 ∘ ◡ 𝐹 )
6		nfcv	⊢ Ⅎ 𝑥 I
7	5 6	nfss	⊢ Ⅎ 𝑥 ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I
8	3 7	nfan	⊢ Ⅎ 𝑥 ( Rel 𝐹 ∧ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I )
9	2 8	nfxfr	⊢ Ⅎ 𝑥 Fun 𝐹