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

Theorem dfss 3342
Description: Variant of subclass definition df-ss 3341. (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 3341 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 eqcom 2444 . 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 1369    i^i cin 3326    C_ wss 3327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-ss 3341
This theorem is referenced by:  dfss2  3344  iinrab2  4232  wefrc  4713  ordtri2or3  4815  onelini  4829  cnvcnv  5289  funimass1  5490  sbthlem5  7424  dmaddpi  9058  dmmulpi  9059  restcldi  18776  cmpsublem  19001  ustuqtop5  19819  tgioo  20372  mdbr3  25700  mdbr4  25701  ssmd1  25714  xrge00  26146  esumpfinvallem  26522  measxun2  26623  eulerpartgbij  26754  bndss  28683
  Copyright terms: Public domain W3C validator