Theorem pssssd 4066

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

Syntax hints:   → wi 4   ⊆ wss 3917   ⊊ wpss 3918

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 3937

This theorem is referenced by:  fin23lem36  10308  fin23lem39  10310  canthnumlem  10608  canthp1lem2  10613  elprnq  10951  npomex  10956  prlem934  10993  ltexprlem7  11002  wuncn  11130  mrieqv2d  17607  slwpss  19549  pgpfac1lem5  20018  lbspss  20996  lsppratlem1  21064  lsppratlem3  21066  lsppratlem4  21067  hashpss  32741  exsslsb  33599  lrelat  39014  lsatcvatlem  39049  oaun3lem1  43370  oaun3lem2  43371