Theorem nfunv

Description: The universal class is not a function. (Contributed by Raph Levien, 27-Jan-2004)

	Ref	Expression
Assertion	nfunv	⊢ ¬ Fun V

Proof

Step	Hyp	Ref	Expression
1		nrelv	⊢ ¬ Rel V
2		funrel	⊢ ( Fun V → Rel V )
3	1 2	mto	⊢ ¬ Fun V