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 ∈ C ∧ F : A ⟶ B → A ∈ V

Proof

Step Hyp Ref Expression
1 fdm ⊢ F : A ⟶ B → dom ⁡ F = A
2 dmexg ⊢ F ∈ C → dom ⁡ F ∈ V
3 eleq1 ⊢ dom ⁡ F = A → dom ⁡ F ∈ V ↔ A ∈ V
4 2 3 syl5ib ⊢ dom ⁡ F = A → F ∈ C → A ∈ V
5 1 4 syl ⊢ F : A ⟶ B → F ∈ C → A ∈ V
6 5 impcom ⊢ F ∈ C ∧ F : A ⟶ B → A ∈ V