Theorem pssssd 4076

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

Syntax hints:   → wi 4   ⊆ wss 3938   ⊊ wpss 3939

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 399  df-pss 3956

This theorem is referenced by:  fin23lem36  9772  fin23lem39  9774  canthnumlem  10072  canthp1lem2  10077  elprnq  10415  npomex  10420  prlem934  10457  ltexprlem7  10466  wuncn  10594  mrieqv2d  16912  slwpss  18739  pgpfac1lem5  19203  lbspss  19856  lsppratlem1  19921  lsppratlem3  19923  lsppratlem4  19924  lrelat  36152  lsatcvatlem  36187