Theorem pssssd 4097

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

Syntax hints:   → wi 4   ⊆ wss 3948   ⊊ wpss 3949

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 3967

This theorem is referenced by:  fin23lem36  10345  fin23lem39  10347  canthnumlem  10645  canthp1lem2  10650  elprnq  10988  npomex  10993  prlem934  11030  ltexprlem7  11039  wuncn  11167  mrieqv2d  17587  slwpss  19521  pgpfac1lem5  19990  lbspss  20837  lsppratlem1  20905  lsppratlem3  20907  lsppratlem4  20908  lrelat  38187  lsatcvatlem  38222  oaun3lem1  42426  oaun3lem2  42427