Description: This somewhat non-intuitive theorem tells us the value of its function
is the empty set when the class C it would otherwise map to is a
proper class. This is a technical lemma that can help eliminate
redundant sethood antecedents otherwise required by fvmptg .
(Contributed by NM, 21-Oct-2003)(Revised by Mario Carneiro, 9-Sep-2013)