Theorem pssssd 4027

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895   ⊊ wpss 4013

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 4014

This theorem is used by:  fin23lem36  10426  fin23lem39  10428  canthnumlem  10733  canthp1lem2  10738  elprnq  11076  npomex  11081  prlem934  11118  ltexprlem7  11127  wuncn  11255  hashpss  14554  mrieqv2d  17813  slwpss  19826  pgpfac1lem5  20295  lbspss  21357  lsppratlem1  21425  lsppratlem3  21427  lsppratlem4  21428  exsslsb  34229  lrelat  40072  lsatcvatlem  40107  oaun3lem1  44376  oaun3lem2  44377