Metamath Proof Explorer

Theorem nev

Description: Express that not every set is in a class. (Contributed by RP, 16-Apr-2020)

Ref Expression
Assertion nev 
|- ( A =/= _V <-> -. A. x x e. A )

Proof

Step Hyp Ref Expression
1 eqv 
 |-  ( A = _V <-> A. x x e. A )
2 1 necon3abii 
 |-  ( A =/= _V <-> -. A. x x e. A )