This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( 𝐵 ∈ V ↔ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V ) )

Proof

Step Hyp Ref Expression
1 fsetex ⊢ ( 𝐵 ∈ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )
2 fsetprcnex ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V )
3 2 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) )
4 df-nel ⊢ ( 𝐵 ∉ V ↔ ¬ 𝐵 ∈ V )
5 df-nel ⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ↔ ¬ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )
6 3 4 5 3imtr3g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( ¬ 𝐵 ∈ V → ¬ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V ) )
7 6 con4d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V → 𝐵 ∈ V ) )
8 1 7 impbid2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( 𝐵 ∈ V ↔ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V ) )