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

Metamath Proof Explorer

Theorem fndmexd

Description: If a function is a set, its domain is a set. (Contributed by Rohan Ridenour, 13-May-2024)

Ref Expression
Hypotheses fndmexd.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
fndmexd.2 ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
Assertion fndmexd ( 𝜑 → 𝐷 ∈ V )

Proof

Step Hyp Ref Expression
1 fndmexd.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2 fndmexd.2 ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
3 2 fndmd ⊢ ( 𝜑 → dom 𝐹 = 𝐷 )
4 1 dmexd ⊢ ( 𝜑 → dom 𝐹 ∈ V )
5 3 4 eqeltrrd ⊢ ( 𝜑 → 𝐷 ∈ V )