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

Theorem dfss4 3416
Description: Subclass defined in terms of class difference. See comments under dfun2 3417. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
dfss4  |-  ( A 
C_  B  <->  ( B  \  ( B  \  A
) )  =  A )

Proof of Theorem dfss4
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 sseqin2 3401 . 2  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
2 eldif 3175 . . . . . . 7  |-  ( x  e.  ( B  \  A )  <->  ( x  e.  B  /\  -.  x  e.  A ) )
32notbii 287 . . . . . 6  |-  ( -.  x  e.  ( B 
\  A )  <->  -.  (
x  e.  B  /\  -.  x  e.  A
) )
43anbi2i 675 . . . . 5  |-  ( ( x  e.  B  /\  -.  x  e.  ( B  \  A ) )  <-> 
( x  e.  B  /\  -.  ( x  e.  B  /\  -.  x  e.  A ) ) )
5 elin 3371 . . . . . 6  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  x  e.  A ) )
6 abai 770 . . . . . 6  |-  ( ( x  e.  B  /\  x  e.  A )  <->  ( x  e.  B  /\  ( x  e.  B  ->  x  e.  A ) ) )
7 iman 413 . . . . . . 7  |-  ( ( x  e.  B  ->  x  e.  A )  <->  -.  ( x  e.  B  /\  -.  x  e.  A
) )
87anbi2i 675 . . . . . 6  |-  ( ( x  e.  B  /\  ( x  e.  B  ->  x  e.  A ) )  <->  ( x  e.  B  /\  -.  (
x  e.  B  /\  -.  x  e.  A
) ) )
95, 6, 83bitri 262 . . . . 5  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  -.  (
x  e.  B  /\  -.  x  e.  A
) ) )
104, 9bitr4i 243 . . . 4  |-  ( ( x  e.  B  /\  -.  x  e.  ( B  \  A ) )  <-> 
x  e.  ( B  i^i  A ) )
1110difeqri 3309 . . 3  |-  ( B 
\  ( B  \  A ) )  =  ( B  i^i  A
)
1211eqeq1i 2303 . 2  |-  ( ( B  \  ( B 
\  A ) )  =  A  <->  ( B  i^i  A )  =  A )
131, 12bitr4i 243 1  |-  ( A 
C_  B  <->  ( B  \  ( B  \  A
) )  =  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696    \ cdif 3162    i^i cin 3164    C_ wss 3165
This theorem is referenced by:  dfin4  3422  sorpsscmpl  6304  sbthlem3  6989  fin23lem7  7958  fin23lem11  7959  compsscnvlem  8012  compssiso  8016  isf34lem4  8019  efgmnvl  15039  isopn2  16785  iincld  16792  iuncld  16798  clsval2  16803  ntrval2  16804  ntrdif  16805  clsdif  16806  cmclsopn  16815  cmntrcld  16816  opncldf1  16837  indiscld  16844  mretopd  16845  restcld  16919  pnrmopn  17087  conndisj  17158  hausllycmp  17236  kqcldsat  17440  filufint  17631  cfinufil  17639  ufilen  17641  alexsublem  17754  bcth3  18769  inmbl  18915  iccmbl  18939  mbfimaicc  19004  i1fd  19052  itgss3  19185  iundifdifd  23175  iundifdif  23176  cldssbrsiga  23533  kur14lem4  23755  itg2addnclem  25003  cldbnd  26347  clsun  26349  fdc  26558  frlmlbs  27352
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-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator