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

Theorem dfss4 3405
Description: Subclass defined in terms of class difference. See comments under dfun2 3406. (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 )
Dummy variable  x is distinct from all other variables.

Proof of Theorem dfss4
StepHypRef Expression
1 sseqin2 3390 . 2  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
2 eldif 3164 . . . . . . 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 677 . . . . 5  |-  ( ( x  e.  B  /\  -.  x  e.  ( B  \  A ) )  <-> 
( x  e.  B  /\  -.  ( x  e.  B  /\  -.  x  e.  A ) ) )
5 elin 3360 . . . . . 6  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  x  e.  A ) )
6 abai 772 . . . . . 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 677 . . . . . 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 3298 . . 3  |-  ( B 
\  ( B  \  A ) )  =  ( B  i^i  A
)
1211eqeq1i 2292 . 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 1624    e. wcel 1685    \ cdif 3151    i^i cin 3153    C_ wss 3154
This theorem is referenced by:  dfin4  3411  sorpsscmpl  6250  sbthlem3  6969  fin23lem7  7938  fin23lem11  7939  compsscnvlem  7992  compssiso  7996  isf34lem4  7999  efgmnvl  15018  isopn2  16764  iincld  16771  iuncld  16777  clsval2  16782  ntrval2  16783  ntrdif  16784  clsdif  16785  cmclsopn  16794  cmntrcld  16795  opncldf1  16816  indiscld  16823  mretopd  16824  restcld  16898  pnrmopn  17066  conndisj  17137  hausllycmp  17215  kqcldsat  17419  filufint  17610  cfinufil  17618  ufilen  17620  alexsublem  17733  bcth3  18748  inmbl  18894  iccmbl  18918  mbfimaicc  18983  i1fd  19031  itgss3  19164  kur14lem4  23145  cldbnd  25644  clsun  25646  fdc  25855  frlmlbs  26649
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-dif 3157  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator