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

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

Proof of Theorem dfss
StepHypRef Expression
1 df-ss 3548 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 eqcom 2611 . 2 ((𝐴𝐵) = 𝐴𝐴 = (𝐴𝐵))
31, 2bitri 262 1 (𝐴𝐵𝐴 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  cin 3533  wss 3534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-cleq 2597  df-ss 3548
This theorem is referenced by:  dfss2  3551  iinrab2  4508  wefrc  5017  cnvcnv  5486  ordtri2or3  5722  onelini  5737  funimass1  5866  sbthlem5  7931  dmaddpi  9563  dmmulpi  9564  restcldi  20724  cmpsublem  20949  ustuqtop5  21796  tgioo  22334  mdbr3  28341  mdbr4  28342  ssmd1  28355  xrge00  28818  esumpfinvallem  29264  measxun2  29401  eulerpartgbij  29562  bndss  32553  dfrcl2  36783  isotone2  37165  restuni4  38134  fourierdlem93  38891  sge0resplit  39098  mbfresmf  39425
  Copyright terms: Public domain W3C validator