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

Metamath Proof Explorer

Theorem funfni

Description: Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004)

Ref Expression
Hypothesis funfni.1 ⊢ Fun ⁡ F ∧ B ∈ dom ⁡ F → φ
Assertion funfni ⊢ F Fn A ∧ B ∈ A → φ

Proof

Step Hyp Ref Expression
1 funfni.1 ⊢ Fun ⁡ F ∧ B ∈ dom ⁡ F → φ
2 fnfun ⊢ F Fn A → Fun ⁡ F
3 fndm ⊢ F Fn A → dom ⁡ F = A
4 3 eleq2d ⊢ F Fn A → B ∈ dom ⁡ F ↔ B ∈ A
5 4 biimpar ⊢ F Fn A ∧ B ∈ A → B ∈ dom ⁡ F
6 2 5 1 syl2an2r ⊢ F Fn A ∧ B ∈ A → φ