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

Theorem dfss 3167
Description: Variant of subclass definition df-ss 3166. (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 3166 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 eqcom 2285 . 2  |-  ( ( A  i^i  B )  =  A  <->  A  =  ( A  i^i  B ) )
31, 2bitri 240 1  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    i^i cin 3151    C_ wss 3152
This theorem is referenced by:  dfss2  3169  iinrab2  3965  wefrc  4387  ordtri2or3  4490  onelini  4504  cnvcnv  5126  funimass1  5325  sbthlem5  6975  dmaddpi  8514  dmmulpi  8515  restcldi  16904  cmpsublem  17126  tgioo  18302  mdbr3  22877  mdbr4  22878  ssmd1  22891  xrge00  23311  esumpfinvallem  23442  measxun2  23538  bndss  26510
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ss 3166
  Copyright terms: Public domain W3C validator