Theorem pssssd 4055

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

Syntax hints:   → wi 4   ⊆ wss 3906   ⊊ wpss 3907

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 209  df-an 400  df-pss 3926

This theorem is referenced by:  fin23lem36  10307  fin23lem39  10309  canthnumlem  10608  canthp1lem2  10613  elprnq  10951  npomex  10956  prlem934  10993  ltexprlem7  11002  wuncn  11130  mrieqv2d  17673  slwpss  19654  pgpfac1lem5  20123  lbspss  21151  lsppratlem1  21219  lsppratlem3  21221  lsppratlem4  21222  hashpss  33013  exsslsb  33896  lrelat  39643  lsatcvatlem  39678  oaun3lem1  43956  oaun3lem2  43957