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