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

Theorem dfss 3555
 Description: Variant of subclass definition df-ss 3554. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
dfss (𝐴𝐵𝐴 = (𝐴𝐵))

Proof of Theorem dfss
StepHypRef Expression
1 df-ss 3554 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 eqcom 2617 . 2 ((𝐴𝐵) = 𝐴𝐴 = (𝐴𝐵))
31, 2bitri 263 1 (𝐴𝐵𝐴 = (𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   = wceq 1475   ∩ cin 3539   ⊆ wss 3540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ss 3554 This theorem is referenced by:  dfss2  3557  iinrab2  4519  wefrc  5032  cnvcnv  5505  ordtri2or3  5741  onelini  5756  funimass1  5885  sbthlem5  7959  dmaddpi  9591  dmmulpi  9592  restcldi  20787  cmpsublem  21012  ustuqtop5  21859  tgioo  22407  mdbr3  28540  mdbr4  28541  ssmd1  28554  xrge00  29017  esumpfinvallem  29463  measxun2  29600  eulerpartgbij  29761  bndss  32755  dfrcl2  36985  isotone2  37367  restuni4  38336  fourierdlem93  39092  sge0resplit  39299  mbfresmf  39626
 Copyright terms: Public domain W3C validator