Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pssss | Structured version Visualization version Unicode 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 3590 | . 2 | |
2 | 1 | simplbi 476 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wne 2794 wss 3574 wpss 3575 |
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 386 df-pss 3590 |
This theorem is referenced by: pssssd 3704 sspss 3706 pssn2lp 3708 psstr 3711 brrpssg 6939 php 8144 php2 8145 php3 8146 pssnn 8178 findcard3 8203 marypha1lem 8339 infpssr 9130 fin4en1 9131 ssfin4 9132 fin23lem34 9168 npex 9808 elnp 9809 suplem1pr 9874 lsmcv 19141 islbs3 19155 obslbs 20074 spansncvi 28511 chrelati 29223 atcvatlem 29244 fundmpss 31664 dfon2lem6 31693 finminlem 32312 psshepw 38082 |
Copyright terms: Public domain | W3C validator |