Metamath Proof Explorer

Theorem nvpss

Description: No class strictly includes the universal class. Dual of npss0 . (Contributed by BJ, 12-Jul-2026)

Ref Expression
Assertion nvpss 
|- -. _V C. A

Proof

Step Hyp Ref Expression
1 ssv 
 |-  A C_ _V
2 ssnpss 
 |-  ( A C_ _V -> -. _V C. A )
3 1 2 ax-mp 
 |-  -. _V C. A