Theorem pssssd 4123

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

Syntax hints:   → wi 4   ⊆ wss 3976   ⊊ wpss 3977

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 3996

This theorem is referenced by:  fin23lem36  10417  fin23lem39  10419  canthnumlem  10717  canthp1lem2  10722  elprnq  11060  npomex  11065  prlem934  11102  ltexprlem7  11111  wuncn  11239  mrieqv2d  17697  slwpss  19654  pgpfac1lem5  20123  lbspss  21104  lsppratlem1  21172  lsppratlem3  21174  lsppratlem4  21175  lrelat  38970  lsatcvatlem  39005  oaun3lem1  43336  oaun3lem2  43337