Theorem pssssd 4050

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

Syntax hints:   → wi 4   ⊆ wss 3899   ⊊ wpss 3900

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 3919

This theorem is referenced by:  fin23lem36  10256  fin23lem39  10258  canthnumlem  10557  canthp1lem2  10562  elprnq  10900  npomex  10905  prlem934  10942  ltexprlem7  10951  wuncn  11079  mrieqv2d  17560  slwpss  19539  pgpfac1lem5  20008  lbspss  21032  lsppratlem1  21100  lsppratlem3  21102  lsppratlem4  21103  hashpss  32838  exsslsb  33702  lrelat  39213  lsatcvatlem  39248  oaun3lem1  43558  oaun3lem2  43559