Metamath Proof Explorer


Theorem fndmexb

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

Ref Expression
Assertion fndmexb ( 𝐹 Fn 𝐴 → ( 𝐴 ∈ V ↔ 𝐹 ∈ V ) )

Proof

Step Hyp Ref Expression
1 fnex ( ( 𝐹 Fn 𝐴𝐴 ∈ V ) → 𝐹 ∈ V )
2 1 ex ( 𝐹 Fn 𝐴 → ( 𝐴 ∈ V → 𝐹 ∈ V ) )
3 simpr ( ( 𝐹 Fn 𝐴𝐹 ∈ V ) → 𝐹 ∈ V )
4 simpl ( ( 𝐹 Fn 𝐴𝐹 ∈ V ) → 𝐹 Fn 𝐴 )
5 3 4 fndmexd ( ( 𝐹 Fn 𝐴𝐹 ∈ V ) → 𝐴 ∈ V )
6 5 ex ( 𝐹 Fn 𝐴 → ( 𝐹 ∈ V → 𝐴 ∈ V ) )
7 2 6 impbid ( 𝐹 Fn 𝐴 → ( 𝐴 ∈ V ↔ 𝐹 ∈ V ) )