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	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐴 ∈ V ↔ 𝐹 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
2		fndmexb	⊢ ( 𝐹 Fn 𝐴 → ( 𝐴 ∈ V ↔ 𝐹 ∈ V ) )
3	1 2	syl	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐴 ∈ V ↔ 𝐹 ∈ V ) )