This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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