Theorem pssssd 4034

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

Syntax hints:   → wi 4   ⊆ wss 3885   ⊊ wpss 3886

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 209  df-an 398  df-pss 3905

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  21076  lsppratlem1  21144  lsppratlem3  21146  lsppratlem4  21147  hashpss  32905  exsslsb  33793  lrelat  39521  lsatcvatlem  39556  oaun3lem1  43834  oaun3lem2  43835