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 3951 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | |
2 | 1 | simplbi 498 | 1 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ≠ wne 3013 ⊆ wss 3933 ⊊ wpss 3934 |
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 208 df-an 397 df-pss 3951 |
This theorem is referenced by: pssssd 4071 sspss 4073 pssn2lp 4075 psstr 4078 brrpssg 7440 php 8689 php2 8690 php3 8691 pssnn 8724 findcard3 8749 marypha1lem 8885 infpssr 9718 fin4en1 9719 ssfin4 9720 fin23lem34 9756 npex 10396 elnp 10397 suplem1pr 10462 lsmcv 19842 islbs3 19856 obslbs 20802 spansncvi 29356 chrelati 30068 atcvatlem 30089 satfun 32555 fundmpss 32906 dfon2lem6 32930 finminlem 33563 fvineqsneq 34575 pssexg 38990 xppss12 38993 psshepw 40012 |
Copyright terms: Public domain | W3C validator |