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

Theorem dfss 3180
Description: Variant of subclass definition df-ss 3179. (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 3179 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 eqcom 2298 . 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 1632    i^i cin 3164    C_ wss 3165
This theorem is referenced by:  dfss2  3182  iinrab2  3981  wefrc  4403  ordtri2or3  4506  onelini  4520  cnvcnv  5142  funimass1  5341  sbthlem5  6991  dmaddpi  8530  dmmulpi  8531  restcldi  16920  cmpsublem  17142  tgioo  18318  mdbr3  22893  mdbr4  22894  ssmd1  22907  xrge00  23326  esumpfinvallem  23457  measxun2  23553  bndss  26613
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ss 3179
  Copyright terms: Public domain W3C validator