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

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

Proof of Theorem dfss
StepHypRef Expression
1 df-ss 3950 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 eqcom 2826 . 2 ((𝐴𝐵) = 𝐴𝐴 = (𝐴𝐵))
31, 2bitri 277 1 (𝐴𝐵𝐴 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 208   = wceq 1530  cin 3933  wss 3934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-cleq 2812  df-ss 3950
This theorem is referenced by:  dfss2  3953  iinrab2  4983  wefrc  5542  cnvcnv  6042  ordtri2or3  6281  onelini  6295  funimass1  6429  sbthlem5  8623  dmaddpi  10304  dmmulpi  10305  smndex1bas  18063  restcldi  21773  cmpsublem  21999  ustuqtop5  22846  tgioo  23396  cphsscph  23846  mdbr3  30066  mdbr4  30067  ssmd1  30080  xrge00  30666  esumpfinvallem  31321  measxun2  31457  eulerpartgbij  31618  reprfz1  31883  bj-ismooredr2  34389  bndss  35051  redundss3  35850  dfrcl2  40004  isotone2  40384  restuni4  41372  fourierdlem93  42469  sge0resplit  42673  mbfresmf  43001
  Copyright terms: Public domain W3C validator