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 3996 | . 2 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3853 ⊊ wpss 3854 |
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 3872 |
This theorem is referenced by: fin23lem36 9860 fin23lem39 9862 canthnumlem 10160 canthp1lem2 10165 elprnq 10503 npomex 10508 prlem934 10545 ltexprlem7 10554 wuncn 10682 mrieqv2d 17025 slwpss 18867 pgpfac1lem5 19332 lbspss 19985 lsppratlem1 20050 lsppratlem3 20052 lsppratlem4 20053 lrelat 36683 lsatcvatlem 36718 |
Copyright terms: Public domain | W3C validator |