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

Theorem sspss 4051
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 4037 . . . . 5 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
21simplbi2 504 . . . 4 (𝐴𝐵 → (¬ 𝐴 = 𝐵𝐴𝐵))
32con1d 147 . . 3 (𝐴𝐵 → (¬ 𝐴𝐵𝐴 = 𝐵))
43orrd 860 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
5 pssss 4047 . . 3 (𝐴𝐵𝐴𝐵)
6 eqimss 3998 . . 3 (𝐴 = 𝐵𝐴𝐵)
75, 6jaoi 854 . 2 ((𝐴𝐵𝐴 = 𝐵) → 𝐴𝐵)
84, 7impbii 212 1 (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wo 844   = wceq 1538  wss 3908  wpss 3909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-ne 3012  df-v 3471  df-in 3915  df-ss 3925  df-pss 3927
This theorem is referenced by:  sspsstri  4054  sspsstr  4057  psssstr  4058  ordsseleq  6198  sorpssuni  7443  sorpssint  7444  ssnnfi  8725  ackbij1b  9650  fin23lem40  9762  zorng  9915  psslinpr  10442  suplem2pr  10464  ressval3d  16552  mrissmrcd  16902  pgpssslw  18730  pgpfac1lem5  19192  idnghm  23347  dfon2lem4  33105  finminlem  33740  lkrss2N  36424  dvh3dim3N  38704
  Copyright terms: Public domain W3C validator