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

Theorem dfss 3476
Description: Variant of subclass definition df-ss 3475. (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 3475 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 eqcom 2452 . 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 1383    i^i cin 3460    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-ss 3475
This theorem is referenced by:  dfss2  3478  iinrab2  4378  wefrc  4863  ordtri2or3  4965  onelini  4979  cnvcnv  5449  funimass1  5651  sbthlem5  7633  dmaddpi  9271  dmmulpi  9272  restcldi  19652  cmpsublem  19877  ustuqtop5  20726  tgioo  21279  mdbr3  27194  mdbr4  27195  ssmd1  27208  xrge00  27652  esumpfinvallem  28058  measxun2  28159  eulerpartgbij  28289  bndss  30258  fourierdlem93  31936
  Copyright terms: Public domain W3C validator