Theorem pssssd 4110

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

Syntax hints:   → wi 4   ⊆ wss 3963   ⊊ wpss 3964

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 3983

This theorem is referenced by:  fin23lem36  10386  fin23lem39  10388  canthnumlem  10686  canthp1lem2  10691  elprnq  11029  npomex  11034  prlem934  11071  ltexprlem7  11080  wuncn  11208  mrieqv2d  17684  slwpss  19645  pgpfac1lem5  20114  lbspss  21099  lsppratlem1  21167  lsppratlem3  21169  lsppratlem4  21170  lrelat  38996  lsatcvatlem  39031  oaun3lem1  43364  oaun3lem2  43365