Theorem pssssd 4051

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902   ⊊ wpss 3903

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 402  df-pss 3922

This theorem is used by:  fin23lem36  10353  fin23lem39  10355  canthnumlem  10658  canthp1lem2  10663  elprnq  11001  npomex  11006  prlem934  11043  ltexprlem7  11052  wuncn  11180  hashpss  14474  mrieqv2d  17729  slwpss  19738  pgpfac1lem5  20207  lbspss  21265  lsppratlem1  21333  lsppratlem3  21335  lsppratlem4  21336  exsslsb  34092  lrelat  39872  lsatcvatlem  39907  oaun3lem1  44200  oaun3lem2  44201