Theorem pssssd 4053

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

Syntax hints:   → wi 4   ⊆ wss 3902   ⊊ wpss 3903

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 3922

This theorem is referenced by:  fin23lem36  10262  fin23lem39  10264  canthnumlem  10563  canthp1lem2  10568  elprnq  10906  npomex  10911  prlem934  10948  ltexprlem7  10957  wuncn  11085  mrieqv2d  17566  slwpss  19545  pgpfac1lem5  20014  lbspss  21038  lsppratlem1  21106  lsppratlem3  21108  lsppratlem4  21109  hashpss  32891  exsslsb  33755  lrelat  39342  lsatcvatlem  39377  oaun3lem1  43683  oaun3lem2  43684