| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pssssd | Structured version Visualization version GIF version | ||
| Description: Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.) |
| Ref | Expression |
|---|---|
| pssssd.1 | ⊢ (𝜑 → 𝐴 ⊊ 𝐵) |
| Ref | Expression |
|---|---|
| pssssd | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pssssd.1 | . 2 ⊢ (𝜑 → 𝐴 ⊊ 𝐵) | |
| 2 | pssss 4098 | . 2 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ⊆ 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: fin23lem36 10388 fin23lem39 10390 canthnumlem 10688 canthp1lem2 10693 elprnq 11031 npomex 11036 prlem934 11073 ltexprlem7 11082 wuncn 11210 mrieqv2d 17682 slwpss 19630 pgpfac1lem5 20099 lbspss 21081 lsppratlem1 21149 lsppratlem3 21151 lsppratlem4 21152 hashpss 32813 exsslsb 33647 lrelat 39015 lsatcvatlem 39050 oaun3lem1 43387 oaun3lem2 43388 |
| Copyright terms: Public domain | W3C validator |