MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pssssd Structured version   Visualization version   GIF version

Theorem pssssd 4100
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
StepHypRef Expression
1 pssssd.1 . 2 (𝜑𝐴𝐵)
2 pssss 4098 . 2 (𝐴𝐵𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3951  wpss 3952
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 3971
This theorem is referenced by:  fin23lem36  10388  fin23lem39  10390  canthnumlem  10688  canthp1lem2  10693  elprnq  11031  npomex  11036  prlem934  11073  ltexprlem7  11082  wuncn  11210  mrieqv2d  17682  slwpss  19630  pgpfac1lem5  20099  lbspss  21081  lsppratlem1  21149  lsppratlem3  21151  lsppratlem4  21152  hashpss  32813  exsslsb  33647  lrelat  39015  lsatcvatlem  39050  oaun3lem1  43387  oaun3lem2  43388
  Copyright terms: Public domain W3C validator