This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹