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 
|- ( ph -> F e. V )
fndmexd.2 
|- ( ph -> F Fn D )
Assertion fndmexd 
|- ( ph -> D e. _V )

Proof

Step Hyp Ref Expression
1 fndmexd.1 
 |-  ( ph -> F e. V )
2 fndmexd.2 
 |-  ( ph -> F Fn D )
3 2 fndmd 
 |-  ( ph -> dom F = D )
4 1 dmexd 
 |-  ( ph -> dom F e. _V )
5 3 4 eqeltrrd 
 |-  ( ph -> D e. _V )