Theorem pssssd 4040

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

Syntax hints:   → wi 4   ⊆ wss 3889   ⊊ wpss 3890

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 3909

This theorem is referenced by:  fin23lem36  10270  fin23lem39  10272  canthnumlem  10571  canthp1lem2  10576  elprnq  10914  npomex  10919  prlem934  10956  ltexprlem7  10965  wuncn  11093  mrieqv2d  17605  slwpss  19587  pgpfac1lem5  20056  lbspss  21077  lsppratlem1  21145  lsppratlem3  21147  lsppratlem4  21148  hashpss  32882  exsslsb  33741  lrelat  39460  lsatcvatlem  39495  oaun3lem1  43802  oaun3lem2  43803