Metamath Proof Explorer

Theorem prcnel

Description: A proper class doesn't belong to any class. (Contributed by Glauco Siliprandi, 17-Aug-2020) (Proof shortened by AV, 14-Nov-2020)

Ref Expression
Assertion prcnel 
|- ( -. A e. _V -> -. A e. V )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 1 con3i 
 |-  ( -. A e. _V -> -. A e. V )