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→FFnA
2 fndmexb ⊢FFnA→A∈V↔F∈V
3 1 2 syl ⊢F:A⟶B→A∈V↔F∈V