Metamath Proof Explorer

Theorem pssv

Description: Any non-universal class is a proper subclass of the universal class. (Contributed by NM, 17-May-1998)

Ref Expression
Assertion pssv 
|- ( A C. _V <-> -. A = _V )

Proof

Step Hyp Ref Expression
1 ssv 
 |-  A C_ _V
2 dfpss2 
 |-  ( A C. _V <-> ( A C_ _V /\ -. A = _V ) )
3 1 2 mpbiran 
 |-  ( A C. _V <-> -. A = _V )