Metamath Proof Explorer


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