Theorem pssssd 3666

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

Syntax hints:   → wi 4   ⊆ wss 3540   ⊊ wpss 3541

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 196  df-an 385  df-pss 3556

This theorem is referenced by:  fin23lem36  9053  fin23lem39  9055  canthnumlem  9349  canthp1lem2  9354  elprnq  9692  npomex  9697  prlem934  9734  ltexprlem7  9743  wuncn  9870  mrieqv2d  16122  slwpss  17850  pgpfac1lem5  18301  lbspss  18903  lsppratlem1  18968  lsppratlem3  18970  lsppratlem4  18971  lrelat  33319  lsatcvatlem  33354