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 B A B

Proof

Step Hyp Ref Expression
1 df-pss A B A B A B
2 1 simplbi A B A B