Theorem fsetdmprc0

Description: The set of functions with a proper class as domain is empty. (Contributed by AV, 22-Aug-2024)

	Ref	Expression
Assertion	fsetdmprc0	⊢ ( 𝐴 ∉ V → { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-nel	⊢ ( 𝐴 ∉ V ↔ ¬ 𝐴 ∈ V )
2		vex	⊢ 𝑓 ∈ V
3	2	a1i	⊢ ( 𝑓 Fn 𝐴 → 𝑓 ∈ V )
4		id	⊢ ( 𝑓 Fn 𝐴 → 𝑓 Fn 𝐴 )
5	3 4	fndmexd	⊢ ( 𝑓 Fn 𝐴 → 𝐴 ∈ V )
6	5	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝑓 Fn 𝐴 )
7	1 6	sylbi	⊢ ( 𝐴 ∉ V → ¬ 𝑓 Fn 𝐴 )
8	7	alrimiv	⊢ ( 𝐴 ∉ V → ∀ 𝑓 ¬ 𝑓 Fn 𝐴 )
9		ab0	⊢ ( { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ ↔ ∀ 𝑓 ¬ 𝑓 Fn 𝐴 )
10	8 9	sylibr	⊢ ( 𝐴 ∉ V → { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ )