![]() |
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 4108 | . 2 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3963 ⊊ wpss 3964 |
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 3983 |
This theorem is referenced by: fin23lem36 10386 fin23lem39 10388 canthnumlem 10686 canthp1lem2 10691 elprnq 11029 npomex 11034 prlem934 11071 ltexprlem7 11080 wuncn 11208 mrieqv2d 17684 slwpss 19645 pgpfac1lem5 20114 lbspss 21099 lsppratlem1 21167 lsppratlem3 21169 lsppratlem4 21170 lrelat 38996 lsatcvatlem 39031 oaun3lem1 43364 oaun3lem2 43365 |
Copyright terms: Public domain | W3C validator |