Theorem pssssd 4072

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

Syntax hints:   → wi 4   ⊆ wss 3934   ⊊ wpss 3935

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 3952

This theorem is referenced by:  fin23lem36  9762  fin23lem39  9764  canthnumlem  10062  canthp1lem2  10067  elprnq  10405  npomex  10410  prlem934  10447  ltexprlem7  10456  wuncn  10584  mrieqv2d  16902  slwpss  18729  pgpfac1lem5  19193  lbspss  19846  lsppratlem1  19911  lsppratlem3  19913  lsppratlem4  19914  lrelat  36142  lsatcvatlem  36177