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

Theorem sspss 4064
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 4050 . . . . 5 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
21simplbi2 502 . . . 4 (𝐴𝐵 → (¬ 𝐴 = 𝐵𝐴𝐵))
32con1d 145 . . 3 (𝐴𝐵 → (¬ 𝐴𝐵𝐴 = 𝐵))
43orrd 862 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
5 pssss 4060 . . 3 (𝐴𝐵𝐴𝐵)
6 eqimss 4005 . . 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 3915  wpss 3916
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 2708
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 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-v 3450  df-in 3922  df-ss 3932  df-pss 3934
This theorem is referenced by:  sspsstri  4067  sspsstr  4070  psssstr  4071  ordsseleq  6351  sorpssuni  7674  sorpssint  7675  ssnnfi  9120  ssnnfiOLD  9121  ackbij1b  10182  fin23lem40  10294  zorng  10447  psslinpr  10974  suplem2pr  10996  ressval3d  17134  ressval3dOLD  17135  mrissmrcd  17527  pgpssslw  19403  pgpfac1lem5  19865  idnghm  24123  dfon2lem4  34400  finminlem  34819  lkrss2N  37660  dvh3dim3N  39941
  Copyright terms: Public domain W3C validator