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

Theorem dfss 3970
Description: Variant of subclass definition dfss2 3969. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
dfss (𝐴𝐵𝐴 = (𝐴𝐵))

Proof of Theorem dfss
StepHypRef Expression
1 dfss2 3969 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 eqcom 2744 . 2 ((𝐴𝐵) = 𝐴𝐴 = (𝐴𝐵))
31, 2bitri 275 1 (𝐴𝐵𝐴 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  cin 3950  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-in 3958  df-ss 3968
This theorem is referenced by:  iinrab2  5070  wefrc  5679  cnvcnv  6212  ordtri2or3  6484  onelini  6502  funimass1  6648  sbthlem5  9127  dmaddpi  10930  dmmulpi  10931  smndex1bas  18919  restcldi  23181  cmpsublem  23407  ustuqtop5  24254  tgioo  24817  cphsscph  25285  mdbr3  32316  mdbr4  32317  ssmd1  32330  xrge00  33017  esumpfinvallem  34075  measxun2  34211  eulerpartgbij  34374  reprfz1  34639  bj-ismooredr2  37111  bndss  37793  redundss3  38629  dfrcl2  43687  isotone2  44062  wfac8prim  45019  restuni4  45126  fourierdlem93  46214  sge0resplit  46421  mbfresmf  46754
  Copyright terms: Public domain W3C validator