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 4030 | . 2 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3887 ⊊ wpss 3888 |
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 206 df-an 397 df-pss 3906 |
This theorem is referenced by: fin23lem36 10104 fin23lem39 10106 canthnumlem 10404 canthp1lem2 10409 elprnq 10747 npomex 10752 prlem934 10789 ltexprlem7 10798 wuncn 10926 mrieqv2d 17348 slwpss 19217 pgpfac1lem5 19682 lbspss 20344 lsppratlem1 20409 lsppratlem3 20411 lsppratlem4 20412 lrelat 37028 lsatcvatlem 37063 |
Copyright terms: Public domain | W3C validator |