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 e. _V <-> F e. _V ) )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : A --> B -> F Fn A )
2 fndmexb 
 |-  ( F Fn A -> ( A e. _V <-> F e. _V ) )
3 1 2 syl 
 |-  ( F : A --> B -> ( A e. _V <-> F e. _V ) )