Theorem pssssd 4047

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 4045	. 2 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3897   ⊊ wpss 3898

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 3917

This theorem is referenced by:  fin23lem36  10239  fin23lem39  10241  canthnumlem  10539  canthp1lem2  10544  elprnq  10882  npomex  10887  prlem934  10924  ltexprlem7  10933  wuncn  11061  mrieqv2d  17545  slwpss  19524  pgpfac1lem5  19993  lbspss  21016  lsppratlem1  21084  lsppratlem3  21086  lsppratlem4  21087  hashpss  32791  exsslsb  33609  lrelat  39112  lsatcvatlem  39147  oaun3lem1  43466  oaun3lem2  43467