Theorem pssssd 4048

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899   ⊊ wpss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-pss 3919

This theorem is used by:  fin23lem36  10383  fin23lem39  10385  canthnumlem  10690  canthp1lem2  10695  elprnq  11033  npomex  11038  prlem934  11075  ltexprlem7  11084  wuncn  11212  hashpss  14507  mrieqv2d  17760  slwpss  19773  pgpfac1lem5  20242  lbspss  21304  lsppratlem1  21372  lsppratlem3  21374  lsppratlem4  21375  exsslsb  34148  lrelat  39985  lsatcvatlem  40020  oaun3lem1  44313  oaun3lem2  44314