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 \land B \in dom F) \to φ$
	Assertion	funfni	$⊢ (F Fn A \land B \in A) \to φ$

Step	Hyp	Ref	Expression
1		funfni.1	$⊢ (Fun F \land B \in dom F) \to φ$
2		fnfun	$⊢ F Fn A \to Fun F$
3		fndm	$⊢ F Fn A \to dom F = A$
4	3	eleq2d	$⊢ F Fn A \to (B \in dom F \leftrightarrow B \in A)$
5	4	biimpar	$⊢ (F Fn A \land B \in A) \to B \in dom F$
6	2 5 1	syl2an2r	$⊢ (F Fn A \land B \in A) \to φ$