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

Theorem dfss 3404
Description: Variant of subclass definition df-ss 3403. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
dfss  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )

Proof of Theorem dfss
StepHypRef Expression
1 df-ss 3403 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 eqcom 2391 . 2  |-  ( ( A  i^i  B )  =  A  <->  A  =  ( A  i^i  B ) )
31, 2bitri 249 1  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1399    i^i cin 3388    C_ wss 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-cleq 2374  df-ss 3403
This theorem is referenced by:  dfss2  3406  iinrab2  4306  wefrc  4787  ordtri2or3  4889  onelini  4903  cnvcnv  5368  funimass1  5569  sbthlem5  7550  dmaddpi  9179  dmmulpi  9180  restcldi  19760  cmpsublem  19985  ustuqtop5  20833  tgioo  21386  mdbr3  27332  mdbr4  27333  ssmd1  27346  xrge00  27827  esumpfinvallem  28222  measxun2  28337  eulerpartgbij  28494  bndss  30448  fourierdlem93  32148  dfrcl2  38211
  Copyright terms: Public domain W3C validator