![]() |
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 3964 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | |
2 | 1 | simplbi 496 | 1 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ≠ wne 2929 ⊆ wss 3944 ⊊ wpss 3945 |
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 206 df-an 395 df-pss 3964 |
This theorem is referenced by: pssssd 4093 sspss 4095 pssn2lp 4097 psstr 4100 brrpssg 7731 pssnn 9196 php 9238 php2 9239 php3 9240 phpOLD 9250 php2OLD 9251 php3OLD 9252 pssnnOLD 9293 findcard3 9313 findcard3OLD 9314 marypha1lem 9463 infpssr 10338 fin4en1 10339 ssfin4 10340 fin23lem34 10376 npex 11016 elnp 11017 suplem1pr 11082 lsmcv 21046 islbs3 21060 obslbs 21686 spansncvi 31539 chrelati 32251 atcvatlem 32272 satfun 35154 fundmpss 35495 dfon2lem6 35517 finminlem 35935 fvineqsneq 37024 pssexg 41850 xppss12 41853 psshepw 43362 |
Copyright terms: Public domain | W3C validator |