Theorem pssssd 4059

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

Syntax hints:   → wi 4   ⊆ wss 3911   ⊊ wpss 3912

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 3931

This theorem is referenced by:  fin23lem36  10277  fin23lem39  10279  canthnumlem  10577  canthp1lem2  10582  elprnq  10920  npomex  10925  prlem934  10962  ltexprlem7  10971  wuncn  11099  mrieqv2d  17580  slwpss  19526  pgpfac1lem5  19995  lbspss  21021  lsppratlem1  21089  lsppratlem3  21091  lsppratlem4  21092  hashpss  32784  exsslsb  33585  lrelat  39000  lsatcvatlem  39035  oaun3lem1  43356  oaun3lem2  43357