Metamath Proof Explorer

Theorem fsetcdmex

Description: The class of all functions from a nonempty set A into a class B is a set iff B is a set . (Contributed by AV, 15-Sep-2024)

Ref Expression
Assertion fsetcdmex ⊢ A ∈ V ∧ A ≠ ∅ → B ∈ V ↔ f | f : A ⟶ B ∈ V

Proof

Step Hyp Ref Expression
1 fsetex ⊢ B ∈ V → f | f : A ⟶ B ∈ V
2 fsetprcnex ⊢ A ∈ V ∧ A ≠ ∅ ∧ B ∉ V → f | f : A ⟶ B ∉ V
3 2 ex ⊢ A ∈ V ∧ A ≠ ∅ → B ∉ V → f | f : A ⟶ B ∉ V
4 df-nel ⊢ B ∉ V ↔ ¬ B ∈ V
5 df-nel ⊢ f | f : A ⟶ B ∉ V ↔ ¬ f | f : A ⟶ B ∈ V
6 3 4 5 3imtr3g ⊢ A ∈ V ∧ A ≠ ∅ → ¬ B ∈ V → ¬ f | f : A ⟶ B ∈ V
7 6 con4d ⊢ A ∈ V ∧ A ≠ ∅ → f | f : A ⟶ B ∈ V → B ∈ V
8 1 7 impbid2 ⊢ A ∈ V ∧ A ≠ ∅ → B ∈ V ↔ f | f : A ⟶ B ∈ V