Theorem pssssd 4025

Description: Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.)

Hypothesis

Ref	Expression
pssssd.1	⊢ (𝜑 → 𝐴 ⊊ 𝐵)

Assertion

Ref	Expression
pssssd	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Proof of Theorem pssssd

Step	Hyp	Ref	Expression
1		pssssd.1	. 2 ⊢ (𝜑 → 𝐴 ⊊ 𝐵)
2		pssss 4023	. 2 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3881   ⊊ wpss 3882

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 3900

This theorem is referenced by:  fin23lem36  9759  fin23lem39  9761  canthnumlem  10059  canthp1lem2  10064  elprnq  10402  npomex  10407  prlem934  10444  ltexprlem7  10453  wuncn  10581  mrieqv2d  16902  slwpss  18729  pgpfac1lem5  19194  lbspss  19847  lsppratlem1  19912  lsppratlem3  19914  lsppratlem4  19915  lrelat  36310  lsatcvatlem  36345