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

Theorem sspss 3903
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 3889 . . . . 5 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
21simplbi2 495 . . . 4 (𝐴𝐵 → (¬ 𝐴 = 𝐵𝐴𝐵))
32con1d 142 . . 3 (𝐴𝐵 → (¬ 𝐴𝐵𝐴 = 𝐵))
43orrd 890 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
5 pssss 3899 . . 3 (𝐴𝐵𝐴𝐵)
6 eqimss 3853 . . 3 (𝐴 = 𝐵𝐴𝐵)
75, 6jaoi 884 . 2 ((𝐴𝐵𝐴 = 𝐵) → 𝐴𝐵)
84, 7impbii 201 1 (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198  wo 874   = wceq 1653  wss 3769  wpss 3770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-ne 2972  df-in 3776  df-ss 3783  df-pss 3785
This theorem is referenced by:  sspsstri  3906  sspsstr  3909  psssstr  3910  ordsseleq  5970  sorpssuni  7180  sorpssint  7181  ssnnfi  8421  ackbij1b  9349  fin23lem40  9461  zorng  9614  psslinpr  10141  suplem2pr  10163  ressval3d  16262  ressval3dOLD  16263  mrissmrcd  16615  pgpssslw  18342  pgpfac1lem5  18794  idnghm  22875  dfon2lem4  32203  finminlem  32825  lkrss2N  35190  dvh3dim3N  37470
  Copyright terms: Public domain W3C validator