Metamath Proof Explorer


Theorem fdmexb

Description: The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024)

Ref Expression
Assertion fdmexb F : A B A V F V

Proof

Step Hyp Ref Expression
1 ffn F : A B F Fn A
2 fndmexb F Fn A A V F V
3 1 2 syl F : A B A V F V