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 ABAB

Proof

Step Hyp Ref Expression
1 df-pss ABABAB
2 1 simplbi ABAB