Theorem pssssd 4054

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 4052	. 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  10272  fin23lem39  10274  canthnumlem  10573  canthp1lem2  10578  elprnq  10916  npomex  10921  prlem934  10958  ltexprlem7  10967  wuncn  11095  mrieqv2d  17576  slwpss  19558  pgpfac1lem5  20027  lbspss  21051  lsppratlem1  21119  lsppratlem3  21121  lsppratlem4  21122  hashpss  32906  exsslsb  33780  lrelat  39419  lsatcvatlem  39454  oaun3lem1  43760  oaun3lem2  43761