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

Theorem sspss 3663
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 3649 . . . . 5 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
21simplbi2 652 . . . 4 (𝐴𝐵 → (¬ 𝐴 = 𝐵𝐴𝐵))
32con1d 137 . . 3 (𝐴𝐵 → (¬ 𝐴𝐵𝐴 = 𝐵))
43orrd 391 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
5 pssss 3659 . . 3 (𝐴𝐵𝐴𝐵)
6 eqimss 3615 . . 3 (𝐴 = 𝐵𝐴𝐵)
75, 6jaoi 392 . 2 ((𝐴𝐵𝐴 = 𝐵) → 𝐴𝐵)
84, 7impbii 197 1 (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wo 381   = wceq 1474  wss 3535  wpss 3536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-ne 2777  df-in 3542  df-ss 3549  df-pss 3551
This theorem is referenced by:  sspsstri  3666  sspsstr  3669  psssstr  3670  ordsseleq  5651  sorpssuni  6817  sorpssint  6818  ssnnfi  8037  ackbij1b  8917  fin23lem40  9029  zorng  9182  psslinpr  9705  suplem2pr  9727  ressval3d  15706  mrissmrcd  16065  pgpssslw  17794  pgpfac1lem5  18243  idnghm  22285  dfon2lem4  30737  finminlem  31284  lkrss2N  33273  dvh3dim3N  35555
  Copyright terms: Public domain W3C validator