Theorem pssssd 4030

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

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

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 4017

This theorem is used by:  fin23lem36  10450  fin23lem39  10452  canthnumlem  10757  canthp1lem2  10762  elprnq  11100  npomex  11105  prlem934  11142  ltexprlem7  11151  wuncn  11279  hashpss  14578  mrieqv2d  17839  slwpss  19853  pgpfac1lem5  20322  lbspss  21384  lsppratlem1  21452  lsppratlem3  21454  lsppratlem4  21455  exsslsb  34296  lrelat  40262  lsatcvatlem  40297  oaun3lem1  44566  oaun3lem2  44567