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 4070 | . 2 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3934 ⊊ wpss 3935 |
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 209 df-an 399 df-pss 3952 |
This theorem is referenced by: fin23lem36 9762 fin23lem39 9764 canthnumlem 10062 canthp1lem2 10067 elprnq 10405 npomex 10410 prlem934 10447 ltexprlem7 10456 wuncn 10584 mrieqv2d 16902 slwpss 18729 pgpfac1lem5 19193 lbspss 19846 lsppratlem1 19911 lsppratlem3 19913 lsppratlem4 19914 lrelat 36142 lsatcvatlem 36177 |
Copyright terms: Public domain | W3C validator |