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	|- ( A e/ _V -> { f | f Fn A } = (/) )

Proof

Step	Hyp	Ref	Expression
1		df-nel	|- ( A e/ _V <-> -. A e. _V )
2		vex	|- f e. _V
3	2	a1i	|- ( f Fn A -> f e. _V )
4		id	|- ( f Fn A -> f Fn A )
5	3 4	fndmexd	|- ( f Fn A -> A e. _V )
6	5	con3i	|- ( -. A e. _V -> -. f Fn A )
7	1 6	sylbi	|- ( A e/ _V -> -. f Fn A )
8	7	alrimiv	|- ( A e/ _V -> A. f -. f Fn A )
9		ab0	|- ( { f | f Fn A } = (/) <-> A. f -. f Fn A )
10	8 9	sylibr	|- ( A e/ _V -> { f | f Fn A } = (/) )