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 ) )