Theorem pssssd 4041

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

Syntax hints:   → wi 4   ⊆ wss 3890   ⊊ wpss 3891

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 3910

This theorem is referenced by:  fin23lem36  10265  fin23lem39  10267  canthnumlem  10566  canthp1lem2  10571  elprnq  10909  npomex  10914  prlem934  10951  ltexprlem7  10960  wuncn  11088  mrieqv2d  17600  slwpss  19582  pgpfac1lem5  20051  lbspss  21073  lsppratlem1  21141  lsppratlem3  21143  lsppratlem4  21144  hashpss  32901  exsslsb  33760  lrelat  39478  lsatcvatlem  39513  oaun3lem1  43824  oaun3lem2  43825