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

Theorem dfss 3486
Description: Variant of subclass definition df-ss 3485. (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 3485 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 eqcom 2471 . 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 1374    i^i cin 3470    C_ wss 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-cleq 2454  df-ss 3485
This theorem is referenced by:  dfss2  3488  iinrab2  4383  wefrc  4868  ordtri2or3  4970  onelini  4984  cnvcnv  5452  funimass1  5654  sbthlem5  7623  dmaddpi  9259  dmmulpi  9260  restcldi  19435  cmpsublem  19660  ustuqtop5  20478  tgioo  21031  mdbr3  26880  mdbr4  26881  ssmd1  26894  xrge00  27324  esumpfinvallem  27708  measxun2  27809  eulerpartgbij  27939  bndss  29874  fourierdlem93  31457
  Copyright terms: Public domain W3C validator