| 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 3971 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | |
| 2 | 1 | simplbi 497 | 1 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ≠ wne 2940 ⊆ wss 3951 ⊊ wpss 3952 |
| 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 207 df-an 396 df-pss 3971 |
| This theorem is referenced by: pssssd 4100 sspss 4102 pssn2lp 4104 psstr 4107 brrpssg 7745 pssnn 9208 php 9247 php2 9248 php3 9249 phpOLD 9259 php2OLD 9260 php3OLD 9261 findcard3 9318 findcard3OLD 9319 marypha1lem 9473 infpssr 10348 fin4en1 10349 ssfin4 10350 fin23lem34 10386 npex 11026 elnp 11027 suplem1pr 11092 lsmcv 21143 islbs3 21157 obslbs 21750 spansncvi 31671 chrelati 32383 atcvatlem 32404 satfun 35416 fundmpss 35767 dfon2lem6 35789 finminlem 36319 fvineqsneq 37413 pssexg 42265 xppss12 42268 psshepw 43801 |
| Copyright terms: Public domain | W3C validator |