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 18	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3905   ⊊ wpss 3906

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 401  df-pss 3925

This theorem is used by:  fin23lem36  10336  fin23lem39  10338  canthnumlem  10637  canthp1lem2  10642  elprnq  10980  npomex  10985  prlem934  11022  ltexprlem7  11031  wuncn  11159  hashpss  14451  mrieqv2d  17699  slwpss  19686  pgpfac1lem5  20155  lbspss  21212  lsppratlem1  21280  lsppratlem3  21282  lsppratlem4  21283  exsslsb  33996  lrelat  39816  lsatcvatlem  39851  oaun3lem1  44129  oaun3lem2  44130