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

Theorem dfss 3335
Description: Variant of subclass definition df-ss 3334. (Contributed by NM, 3-Sep-2004.)
Assertion
Ref Expression
dfss  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )

Proof of Theorem dfss
StepHypRef Expression
1 df-ss 3334 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 eqcom 2438 . 2  |-  ( ( A  i^i  B )  =  A  <->  A  =  ( A  i^i  B ) )
31, 2bitri 241 1  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1652    i^i cin 3319    C_ wss 3320
This theorem is referenced by:  dfss2  3337  iinrab2  4154  wefrc  4576  ordtri2or3  4679  onelini  4693  cnvcnv  5323  funimass1  5526  sbthlem5  7221  dmaddpi  8767  dmmulpi  8768  restcldi  17237  cmpsublem  17462  ustuqtop5  18275  tgioo  18827  mdbr3  23800  mdbr4  23801  ssmd1  23814  xrge00  24208  esumpfinvallem  24464  measxun2  24564  bndss  26495
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-cleq 2429  df-ss 3334
  Copyright terms: Public domain W3C validator