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

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
StepHypRef Expression
1 pssssd.1 . 2 (𝜑𝐴𝐵)
2 pssss 4108 . 2 (𝐴𝐵𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator