Theorem pssssd 4062

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

Syntax hints:   → wi 4   ⊆ wss 3913   ⊊ wpss 3914

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 206  df-an 397  df-pss 3932

This theorem is referenced by:  fin23lem36  10293  fin23lem39  10295  canthnumlem  10593  canthp1lem2  10598  elprnq  10936  npomex  10941  prlem934  10978  ltexprlem7  10987  wuncn  11115  mrieqv2d  17533  slwpss  19408  pgpfac1lem5  19872  lbspss  20600  lsppratlem1  20667  lsppratlem3  20669  lsppratlem4  20670  lrelat  37549  lsatcvatlem  37584  oaun3lem1  41767  oaun3lem2  41768