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