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

Theorem sspss 3739
 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 3725 . . . . 5 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
21simplbi2 654 . . . 4 (𝐴𝐵 → (¬ 𝐴 = 𝐵𝐴𝐵))
32con1d 139 . . 3 (𝐴𝐵 → (¬ 𝐴𝐵𝐴 = 𝐵))
43orrd 392 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
5 pssss 3735 . . 3 (𝐴𝐵𝐴𝐵)
6 eqimss 3690 . . 3 (𝐴 = 𝐵𝐴𝐵)
75, 6jaoi 393 . 2 ((𝐴𝐵𝐴 = 𝐵) → 𝐴𝐵)
84, 7impbii 199 1 (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 196   ∨ wo 382   = wceq 1523   ⊆ wss 3607   ⊊ wpss 3608 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ne 2824  df-in 3614  df-ss 3621  df-pss 3623 This theorem is referenced by:  sspsstri  3742  sspsstr  3745  psssstr  3746  ordsseleq  5790  sorpssuni  6988  sorpssint  6989  ssnnfi  8220  ackbij1b  9099  fin23lem40  9211  zorng  9364  psslinpr  9891  suplem2pr  9913  ressval3d  15984  mrissmrcd  16347  pgpssslw  18075  pgpfac1lem5  18524  idnghm  22594  dfon2lem4  31815  finminlem  32437  lkrss2N  34774  dvh3dim3N  37055
 Copyright terms: Public domain W3C validator