Theorem pssssd 4063

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

Syntax hints:   → wi 4   ⊆ wss 3914   ⊊ wpss 3915

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 207  df-an 396  df-pss 3934

This theorem is referenced by:  fin23lem36  10301  fin23lem39  10303  canthnumlem  10601  canthp1lem2  10606  elprnq  10944  npomex  10949  prlem934  10986  ltexprlem7  10995  wuncn  11123  mrieqv2d  17600  slwpss  19542  pgpfac1lem5  20011  lbspss  20989  lsppratlem1  21057  lsppratlem3  21059  lsppratlem4  21060  hashpss  32734  exsslsb  33592  lrelat  39007  lsatcvatlem  39042  oaun3lem1  43363  oaun3lem2  43364