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

Theorem sspss 4099
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 4085 . . . . 5 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
21simplbi2 501 . . . 4 (𝐴𝐵 → (¬ 𝐴 = 𝐵𝐴𝐵))
32con1d 145 . . 3 (𝐴𝐵 → (¬ 𝐴𝐵𝐴 = 𝐵))
43orrd 861 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
5 pssss 4095 . . 3 (𝐴𝐵𝐴𝐵)
6 eqimss 4040 . . 3 (𝐴 = 𝐵𝐴𝐵)
75, 6jaoi 855 . 2 ((𝐴𝐵𝐴 = 𝐵) → 𝐴𝐵)
84, 7impbii 208 1 (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wo 845   = wceq 1541  wss 3948  wpss 3949
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-v 3476  df-in 3955  df-ss 3965  df-pss 3967
This theorem is referenced by:  sspsstri  4102  sspsstr  4105  psssstr  4106  ordsseleq  6393  sorpssuni  7721  sorpssint  7722  ssnnfi  9168  ssnnfiOLD  9169  ackbij1b  10233  fin23lem40  10345  zorng  10498  psslinpr  11025  suplem2pr  11047  ressval3d  17190  ressval3dOLD  17191  mrissmrcd  17583  pgpssslw  19481  pgpfac1lem5  19948  idnghm  24259  dfon2lem4  34753  finminlem  35198  lkrss2N  38034  dvh3dim3N  40315  ordsssucb  42075
  Copyright terms: Public domain W3C validator