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

Metamath Proof Explorer

Theorem nff

Description: Bound-variable hypothesis builder for a mapping. (Contributed by NM, 29-Jan-2004) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses nff.1 ⊢ Ⅎ _ x F
nff.2 ⊢ Ⅎ _ x A
nff.3 ⊢ Ⅎ _ x B
Assertion nff ⊢ Ⅎ x F : A ⟶ B

Proof

Step Hyp Ref Expression
1 nff.1 ⊢ Ⅎ _ x F
2 nff.2 ⊢ Ⅎ _ x A
3 nff.3 ⊢ Ⅎ _ x B
4 df-f ⊢ F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B
5 1 2 nffn ⊢ Ⅎ x F Fn A
6 1 nfrn ⊢ Ⅎ _ x ran ⁡ F
7 6 3 nfss ⊢ Ⅎ x ran ⁡ F ⊆ B
8 5 7 nfan ⊢ Ⅎ x F Fn A ∧ ran ⁡ F ⊆ B
9 4 8 nfxfr ⊢ Ⅎ x F : A ⟶ B