Theorem pssssd 3704

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

Syntax hints:   → wi 4   ⊆ wss 3574   ⊊ wpss 3575

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 197  df-an 386  df-pss 3590

This theorem is referenced by:  fin23lem36  9170  fin23lem39  9172  canthnumlem  9470  canthp1lem2  9475  elprnq  9813  npomex  9818  prlem934  9855  ltexprlem7  9864  wuncn  9991  mrieqv2d  16299  slwpss  18027  pgpfac1lem5  18478  lbspss  19082  lsppratlem1  19147  lsppratlem3  19149  lsppratlem4  19150  lrelat  34301  lsatcvatlem  34336