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

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

Proof of Theorem dfss
StepHypRef Expression
1 df-ss 3581 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 eqcom 2627 . 2 ((𝐴𝐵) = 𝐴𝐴 = (𝐴𝐵))
31, 2bitri 264 1 (𝐴𝐵𝐴 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1481  cin 3566  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613  df-ss 3581
This theorem is referenced by:  dfss2  3584  iinrab2  4574  wefrc  5098  cnvcnv  5574  cnvcnvOLD  5575  ordtri2or3  5812  onelini  5827  funimass1  5959  sbthlem5  8059  dmaddpi  9697  dmmulpi  9698  restcldi  20958  cmpsublem  21183  ustuqtop5  22030  tgioo  22580  mdbr3  29126  mdbr4  29127  ssmd1  29140  xrge00  29660  esumpfinvallem  30110  measxun2  30247  eulerpartgbij  30408  reprfz1  30676  bndss  33556  dfrcl2  37785  isotone2  38167  restuni4  39124  fourierdlem93  40179  sge0resplit  40386  mbfresmf  40711
  Copyright terms: Public domain W3C validator