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

Theorem sspss 4101
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 4087 . . . . 5 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
21simplbi2 500 . . . 4 (𝐴𝐵 → (¬ 𝐴 = 𝐵𝐴𝐵))
32con1d 145 . . 3 (𝐴𝐵 → (¬ 𝐴𝐵𝐴 = 𝐵))
43orrd 863 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
5 pssss 4097 . . 3 (𝐴𝐵𝐴𝐵)
6 eqimss 4041 . . 3 (𝐴 = 𝐵𝐴𝐵)
75, 6jaoi 857 . 2 ((𝐴𝐵𝐴 = 𝐵) → 𝐴𝐵)
84, 7impbii 209 1 (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wo 847   = wceq 1539  wss 3950  wpss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-cleq 2728  df-ne 2940  df-ss 3967  df-pss 3970
This theorem is referenced by:  sspsstri  4104  sspsstr  4107  psssstr  4108  ordsseleq  6412  sorpssuni  7753  sorpssint  7754  ssnnfi  9210  ackbij1b  10279  fin23lem40  10392  zorng  10545  psslinpr  11072  suplem2pr  11094  ressval3d  17293  mrissmrcd  17684  pgpssslw  19633  pgpfac1lem5  20100  idnghm  24765  slelss  27947  dfon2lem4  35788  finminlem  36320  lkrss2N  39171  dvh3dim3N  41452  ordsssucb  43353
  Copyright terms: Public domain W3C validator