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	|- g e. _V
3	2	a1i	|- ( g Fn A -> g e. _V )
4		id	|- ( g Fn A -> g Fn A )
5	3 4	fndmexd	|- ( g Fn A -> A e. _V )
6	5	con3i	|- ( -. A e. _V -> -. g Fn A )
7	1 6	sylbi	|- ( A e/ _V -> -. g Fn A )
8	7	alrimiv	|- ( A e/ _V -> A. g -. g Fn A )
9		fneq1	|- ( f = g -> ( f Fn A <-> g Fn A ) )
10	9	ab0w	|- ( { f | f Fn A } = (/) <-> A. g -. g Fn A )
11	8 10	sylibr	|- ( A e/ _V -> { f | f Fn A } = (/) )