Theorem pssssd 4051

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

Syntax hints:   → wi 4   ⊆ wss 3903   ⊊ wpss 3904

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 3923

This theorem is referenced by:  fin23lem36  10242  fin23lem39  10244  canthnumlem  10542  canthp1lem2  10547  elprnq  10885  npomex  10890  prlem934  10927  ltexprlem7  10936  wuncn  11064  mrieqv2d  17545  slwpss  19491  pgpfac1lem5  19960  lbspss  20986  lsppratlem1  21054  lsppratlem3  21056  lsppratlem4  21057  hashpss  32755  exsslsb  33569  lrelat  39003  lsatcvatlem  39038  oaun3lem1  43357  oaun3lem2  43358