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

Theorem sspss 4112
Description: Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.)
Assertion
Ref Expression
sspss (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵))

Proof of Theorem sspss
StepHypRef Expression
1 dfpss2 4098 . . . . 5 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
21simplbi2 500 . . . 4 (𝐴𝐵 → (¬ 𝐴 = 𝐵𝐴𝐵))
32con1d 145 . . 3 (𝐴𝐵 → (¬ 𝐴𝐵𝐴 = 𝐵))
43orrd 863 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
5 pssss 4108 . . 3 (𝐴𝐵𝐴𝐵)
6 eqimss 4054 . . 3 (𝐴 = 𝐵𝐴𝐵)
75, 6jaoi 857 . 2 ((𝐴𝐵𝐴 = 𝐵) → 𝐴𝐵)
84, 7impbii 209 1 (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wo 847   = wceq 1537  wss 3963  wpss 3964
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-cleq 2727  df-ne 2939  df-ss 3980  df-pss 3983
This theorem is referenced by:  sspsstri  4115  sspsstr  4118  psssstr  4119  ordsseleq  6415  sorpssuni  7751  sorpssint  7752  ssnnfi  9208  ackbij1b  10276  fin23lem40  10389  zorng  10542  psslinpr  11069  suplem2pr  11091  ressval3d  17292  ressval3dOLD  17293  mrissmrcd  17685  pgpssslw  19647  pgpfac1lem5  20114  idnghm  24780  slelss  27961  dfon2lem4  35768  finminlem  36301  lkrss2N  39151  dvh3dim3N  41432  ordsssucb  43325
  Copyright terms: Public domain W3C validator