Theorem pssssd 3901

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

Syntax hints:   → wi 4   ⊆ wss 3769   ⊊ wpss 3770

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 199  df-an 386  df-pss 3785

This theorem is referenced by:  fin23lem36  9458  fin23lem39  9460  canthnumlem  9758  canthp1lem2  9763  elprnq  10101  npomex  10106  prlem934  10143  ltexprlem7  10152  wuncn  10279  mrieqv2d  16614  slwpss  18340  pgpfac1lem5  18794  lbspss  19403  lsppratlem1  19470  lsppratlem3  19472  lsppratlem4  19473  lrelat  35035  lsatcvatlem  35070