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

Theorem dfss4 3737
Description: Subclass defined in terms of class difference. See comments under dfun2 3738. (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 3722 . 2  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
2 eldif 3491 . . . . . . 7  |-  ( x  e.  ( B  \  A )  <->  ( x  e.  B  /\  -.  x  e.  A ) )
32notbii 296 . . . . . 6  |-  ( -.  x  e.  ( B 
\  A )  <->  -.  (
x  e.  B  /\  -.  x  e.  A
) )
43anbi2i 694 . . . . 5  |-  ( ( x  e.  B  /\  -.  x  e.  ( B  \  A ) )  <-> 
( x  e.  B  /\  -.  ( x  e.  B  /\  -.  x  e.  A ) ) )
5 elin 3692 . . . . . 6  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  x  e.  A ) )
6 abai 793 . . . . . 6  |-  ( ( x  e.  B  /\  x  e.  A )  <->  ( x  e.  B  /\  ( x  e.  B  ->  x  e.  A ) ) )
7 iman 424 . . . . . . 7  |-  ( ( x  e.  B  ->  x  e.  A )  <->  -.  ( x  e.  B  /\  -.  x  e.  A
) )
87anbi2i 694 . . . . . 6  |-  ( ( x  e.  B  /\  ( x  e.  B  ->  x  e.  A ) )  <->  ( x  e.  B  /\  -.  (
x  e.  B  /\  -.  x  e.  A
) ) )
95, 6, 83bitri 271 . . . . 5  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  -.  (
x  e.  B  /\  -.  x  e.  A
) ) )
104, 9bitr4i 252 . . . 4  |-  ( ( x  e.  B  /\  -.  x  e.  ( B  \  A ) )  <-> 
x  e.  ( B  i^i  A ) )
1110difeqri 3629 . . 3  |-  ( B 
\  ( B  \  A ) )  =  ( B  i^i  A
)
1211eqeq1i 2474 . 2  |-  ( ( B  \  ( B 
\  A ) )  =  A  <->  ( B  i^i  A )  =  A )
131, 12bitr4i 252 1  |-  ( A 
C_  B  <->  ( B  \  ( B  \  A
) )  =  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767    \ cdif 3478    i^i cin 3480    C_ wss 3481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-dif 3484  df-in 3488  df-ss 3495
This theorem is referenced by:  dfin4  3743  sorpsscmpl  6586  sbthlem3  7641  fin23lem7  8708  fin23lem11  8709  compsscnvlem  8762  compssiso  8766  isf34lem4  8769  efgmnvl  16605  frlmlbs  18700  isopn2  19401  iincld  19408  iuncld  19414  clsval2  19419  ntrval2  19420  ntrdif  19421  clsdif  19422  cmclsopn  19431  cmntrcld  19432  opncldf1  19453  indiscld  19460  mretopd  19461  restcld  19541  pnrmopn  19712  conndisj  19785  hausllycmp  19863  kqcldsat  20102  filufint  20289  cfinufil  20297  ufilen  20299  alexsublem  20412  bcth3  21638  inmbl  21820  iccmbl  21844  mbfimaicc  21908  i1fd  21956  itgss3  22089  frgrawopreg2  24866  iundifdifd  27243  iundifdif  27244  cldssbrsiga  27974  kur14lem4  28469  mblfinlem3  29971  mblfinlem4  29972  ismblfin  29973  itg2addnclem  29984  cldbnd  30062  clsun  30064  fdc  30156  lincext2  32493
  Copyright terms: Public domain W3C validator