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

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

Proof of Theorem dfss
StepHypRef Expression
1 df-ss 3621 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 eqcom 2658 . 2 ((𝐴𝐵) = 𝐴𝐴 = (𝐴𝐵))
31, 2bitri 264 1 (𝐴𝐵𝐴 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523  cin 3606  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ss 3621
This theorem is referenced by:  dfss2  3624  iinrab2  4615  wefrc  5137  cnvcnv  5621  cnvcnvOLD  5622  ordtri2or3  5862  onelini  5877  funimass1  6009  sbthlem5  8115  dmaddpi  9750  dmmulpi  9751  restcldi  21025  cmpsublem  21250  ustuqtop5  22096  tgioo  22646  mdbr3  29284  mdbr4  29285  ssmd1  29298  xrge00  29814  esumpfinvallem  30264  measxun2  30401  eulerpartgbij  30562  reprfz1  30830  bndss  33715  dfrcl2  38283  isotone2  38664  restuni4  39618  fourierdlem93  40734  sge0resplit  40941  mbfresmf  41269
  Copyright terms: Public domain W3C validator