Metamath Proof Explorer

Theorem dmfex

Description: If a mapping is a set, its domain is a set. (Contributed by NM, 27-Aug-2006) (Proof shortened by Andrew Salmon, 17-Sep-2011)

		Ref	Expression
	Assertion	dmfex	$⊢ (F \in C \land F : A ⟶ B) \to A \in V$

Step	Hyp	Ref	Expression
1		fdm	$⊢ F : A ⟶ B \to dom F = A$
2		dmexg	$⊢ F \in C \to dom F \in V$
3		eleq1	$⊢ dom F = A \to (dom F \in V \leftrightarrow A \in V)$
4	2 3	imbitrid	$⊢ dom F = A \to (F \in C \to A \in V)$
5	1 4	syl	$⊢ F : A ⟶ B \to (F \in C \to A \in V)$
6	5	impcom	$⊢ (F \in C \land F : A ⟶ B) \to A \in V$