Theorem pssssd 4062

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

Syntax hints:   → wi 4   ⊆ wss 3913   ⊊ wpss 3914

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 210  df-an 401  df-pss 3933

This theorem is referenced by:  fin23lem36  10334  fin23lem39  10336  canthnumlem  10635  canthp1lem2  10640  elprnq  10978  npomex  10983  prlem934  11020  ltexprlem7  11029  wuncn  11157  hashpss  14448  mrieqv2d  17697  slwpss  19684  pgpfac1lem5  20153  lbspss  21183  lsppratlem1  21251  lsppratlem3  21253  lsppratlem4  21254  exsslsb  33934  lrelat  39715  lsatcvatlem  39750  oaun3lem1  44030  oaun3lem2  44031