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

Theorem sspss 4100
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 4086 . . . . 5 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
21simplbi2 502 . . . 4 (𝐴𝐵 → (¬ 𝐴 = 𝐵𝐴𝐵))
32con1d 145 . . 3 (𝐴𝐵 → (¬ 𝐴𝐵𝐴 = 𝐵))
43orrd 862 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
5 pssss 4096 . . 3 (𝐴𝐵𝐴𝐵)
6 eqimss 4041 . . 3 (𝐴 = 𝐵𝐴𝐵)
75, 6jaoi 856 . 2 ((𝐴𝐵𝐴 = 𝐵) → 𝐴𝐵)
84, 7impbii 208 1 (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wo 846   = wceq 1542  wss 3949  wpss 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-in 3956  df-ss 3966  df-pss 3968
This theorem is referenced by:  sspsstri  4103  sspsstr  4106  psssstr  4107  ordsseleq  6394  sorpssuni  7722  sorpssint  7723  ssnnfi  9169  ssnnfiOLD  9170  ackbij1b  10234  fin23lem40  10346  zorng  10499  psslinpr  11026  suplem2pr  11048  ressval3d  17191  ressval3dOLD  17192  mrissmrcd  17584  pgpssslw  19482  pgpfac1lem5  19949  idnghm  24260  dfon2lem4  34758  finminlem  35203  lkrss2N  38039  dvh3dim3N  40320  ordsssucb  42085
  Copyright terms: Public domain W3C validator