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 3890 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | |
2 | 1 | simplbi 501 | 1 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ≠ wne 2940 ⊆ wss 3871 ⊊ wpss 3872 |
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 210 df-an 400 df-pss 3890 |
This theorem is referenced by: pssssd 4017 sspss 4019 pssn2lp 4021 psstr 4024 brrpssg 7518 php 8835 php2 8836 php3 8837 pssnn 8851 pssnnOLD 8900 findcard3 8919 marypha1lem 9054 infpssr 9927 fin4en1 9928 ssfin4 9929 fin23lem34 9965 npex 10605 elnp 10606 suplem1pr 10671 lsmcv 20183 islbs3 20197 obslbs 20697 spansncvi 29738 chrelati 30450 atcvatlem 30471 satfun 33091 fundmpss 33464 dfon2lem6 33488 finminlem 34249 fvineqsneq 35325 pssexg 39922 xppss12 39925 psshepw 41081 |
Copyright terms: Public domain | W3C validator |