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

Metamath Proof Explorer

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 𝐴