![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pssss | Structured version Visualization version GIF version |
Description: A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.) |
Ref | Expression |
---|---|
pssss | ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-pss 3739 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | |
2 | 1 | simplbi 485 | 1 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ≠ wne 2943 ⊆ wss 3723 ⊊ wpss 3724 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 383 df-pss 3739 |
This theorem is referenced by: pssssd 3854 sspss 3856 pssn2lp 3858 psstr 3861 brrpssg 7086 php 8300 php2 8301 php3 8302 pssnn 8334 findcard3 8359 marypha1lem 8495 infpssr 9332 fin4en1 9333 ssfin4 9334 fin23lem34 9370 npex 10010 elnp 10011 suplem1pr 10076 lsmcv 19355 islbs3 19370 obslbs 20291 spansncvi 28851 chrelati 29563 atcvatlem 29584 fundmpss 32002 dfon2lem6 32029 finminlem 32649 pssexg 37774 xppss12 37777 psshepw 38608 |
Copyright terms: Public domain | W3C validator |