Metamath Proof Explorer

Theorem pssss

Description: A proper subclass is a subclass. Theorem 10 of Suppes p. 23. (Contributed by NM, 7-Feb-1996)

Ref Expression
Assertion pssss 
|- ( A C. B -> A C_ B )

Proof

Step Hyp Ref Expression
1 df-pss 
 |-  ( A C. B <-> ( A C_ B /\ A =/= B ) )
2 1 simplbi 
 |-  ( A C. B -> A C_ B )