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

Theorem dfss4 3307
Description: Subclass defined in terms of class difference. See comments under dfun2 3308. (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
StepHypRef Expression
1 sseqin2 3292 . 2  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
2 eldif 3085 . . . . . . 7  |-  ( x  e.  ( B  \  A )  <->  ( x  e.  B  /\  -.  x  e.  A ) )
32notbii 289 . . . . . 6  |-  ( -.  x  e.  ( B 
\  A )  <->  -.  (
x  e.  B  /\  -.  x  e.  A
) )
43anbi2i 678 . . . . 5  |-  ( ( x  e.  B  /\  -.  x  e.  ( B  \  A ) )  <-> 
( x  e.  B  /\  -.  ( x  e.  B  /\  -.  x  e.  A ) ) )
5 elin 3263 . . . . . 6  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  x  e.  A ) )
6 abai 773 . . . . . 6  |-  ( ( x  e.  B  /\  x  e.  A )  <->  ( x  e.  B  /\  ( x  e.  B  ->  x  e.  A ) ) )
7 iman 415 . . . . . . 7  |-  ( ( x  e.  B  ->  x  e.  A )  <->  -.  ( x  e.  B  /\  -.  x  e.  A
) )
87anbi2i 678 . . . . . 6  |-  ( ( x  e.  B  /\  ( x  e.  B  ->  x  e.  A ) )  <->  ( x  e.  B  /\  -.  (
x  e.  B  /\  -.  x  e.  A
) ) )
95, 6, 83bitri 264 . . . . 5  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  -.  (
x  e.  B  /\  -.  x  e.  A
) ) )
104, 9bitr4i 245 . . . 4  |-  ( ( x  e.  B  /\  -.  x  e.  ( B  \  A ) )  <-> 
x  e.  ( B  i^i  A ) )
1110difeqri 3210 . . 3  |-  ( B 
\  ( B  \  A ) )  =  ( B  i^i  A
)
1211eqeq1i 2260 . 2  |-  ( ( B  \  ( B 
\  A ) )  =  A  <->  ( B  i^i  A )  =  A )
131, 12bitr4i 245 1  |-  ( A 
C_  B  <->  ( B  \  ( B  \  A
) )  =  A )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360    = wceq 1619    e. wcel 1621    \ cdif 3072    i^i cin 3074    C_ wss 3075
This theorem is referenced by:  dfin4  3313  sorpsscmpl  6137  sbthlem3  6855  fin23lem7  7823  fin23lem11  7824  compsscnvlem  7877  compssiso  7881  isf34lem4  7884  efgmnvl  14820  isopn2  16563  iincld  16570  iuncld  16576  clsval2  16581  ntrval2  16582  ntrdif  16583  clsdif  16584  cmclsopn  16593  cmntrcld  16594  opncldf1  16615  indiscld  16622  mretopd  16623  restcld  16697  pnrmopn  16865  conndisj  16936  hausllycmp  17014  kqcldsat  17218  filufint  17409  cfinufil  17417  ufilen  17419  alexsublem  17532  bcth3  18547  inmbl  18693  iccmbl  18717  mbfimaicc  18782  i1fd  18830  itgss3  18963  kur14lem4  22840  cldbnd  25339  clsun  25341  fdc  25550  frlmlbs  26344
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2727  df-dif 3078  df-in 3082  df-ss 3086
  Copyright terms: Public domain W3C validator