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 ⊢ Ⅎ _ x F
nffn.2 ⊢ Ⅎ _ x A
Assertion nffn ⊢ Ⅎ x F Fn A

Proof

Step Hyp Ref Expression
1 nffn.1 ⊢ Ⅎ _ x F
2 nffn.2 ⊢ Ⅎ _ x A
3 df-fn ⊢ F Fn A ↔ Fun ⁡ F ∧ dom ⁡ F = A
4 1 nffun ⊢ Ⅎ x Fun ⁡ F
5 1 nfdm ⊢ Ⅎ _ x dom ⁡ F
6 5 2 nfeq ⊢ Ⅎ x dom ⁡ F = A
7 4 6 nfan ⊢ Ⅎ x Fun ⁡ F ∧ dom ⁡ F = A
8 3 7 nfxfr ⊢ Ⅎ x F Fn A