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

Theorem dfss4 3345
Description: Subclass defined in terms of class difference. See comments under dfun2 3346. (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 3330 . 2  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
2 eldif 3104 . . . . . . 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 3300 . . . . . 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 3238 . . 3  |-  ( B 
\  ( B  \  A ) )  =  ( B  i^i  A
)
1211eqeq1i 2263 . 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 3091    i^i cin 3093    C_ wss 3094
This theorem is referenced by:  dfin4  3351  sorpsscmpl  6187  sbthlem3  6906  fin23lem7  7875  fin23lem11  7876  compsscnvlem  7929  compssiso  7933  isf34lem4  7936  efgmnvl  14950  isopn2  16696  iincld  16703  iuncld  16709  clsval2  16714  ntrval2  16715  ntrdif  16716  clsdif  16717  cmclsopn  16726  cmntrcld  16727  opncldf1  16748  indiscld  16755  mretopd  16756  restcld  16830  pnrmopn  16998  conndisj  17069  hausllycmp  17147  kqcldsat  17351  filufint  17542  cfinufil  17550  ufilen  17552  alexsublem  17665  bcth3  18680  inmbl  18826  iccmbl  18850  mbfimaicc  18915  i1fd  18963  itgss3  19096  kur14lem4  23077  cldbnd  25576  clsun  25578  fdc  25787  frlmlbs  26581
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 1927  ax-ext 2237
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-dif 3097  df-in 3101  df-ss 3108
  Copyright terms: Public domain W3C validator