Theorem pssssd 4100

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

Syntax hints:   → wi 4   ⊆ wss 3951   ⊊ wpss 3952

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 3971

This theorem is referenced by:  fin23lem36  10388  fin23lem39  10390  canthnumlem  10688  canthp1lem2  10693  elprnq  11031  npomex  11036  prlem934  11073  ltexprlem7  11082  wuncn  11210  mrieqv2d  17682  slwpss  19630  pgpfac1lem5  20099  lbspss  21081  lsppratlem1  21149  lsppratlem3  21151  lsppratlem4  21152  hashpss  32813  exsslsb  33647  lrelat  39015  lsatcvatlem  39050  oaun3lem1  43387  oaun3lem2  43388