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

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

Proof of Theorem dfss
StepHypRef Expression
1 df-ss 3748 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 eqcom 2772 . 2 ((𝐴𝐵) = 𝐴𝐴 = (𝐴𝐵))
31, 2bitri 266 1 (𝐴𝐵𝐴 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1652  cin 3733  wss 3734
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758  df-ss 3748
This theorem is referenced by:  dfss2  3751  iinrab2  4741  wefrc  5273  cnvcnv  5771  cnvcnvOLD  5772  ordtri2or3  6007  onelini  6021  funimass1  6151  sbthlem5  8283  dmaddpi  9967  dmmulpi  9968  restcldi  21260  cmpsublem  21485  ustuqtop5  22331  tgioo  22881  cphsscph  23331  mdbr3  29615  mdbr4  29616  ssmd1  29629  xrge00  30136  esumpfinvallem  30586  measxun2  30723  eulerpartgbij  30884  reprfz1  31156  bndss  34010  redss3  34801  dfrcl2  38644  isotone2  39024  restuni4  39957  fourierdlem93  41056  sge0resplit  41263  mbfresmf  41591
  Copyright terms: Public domain W3C validator