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

Theorem dfss4 3693
Description: Subclass defined in terms of class difference. See comments under dfun2 3694. (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 3678 . 2  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
2 eldif 3447 . . . . . . 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 3648 . . . . . 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 3585 . . 3  |-  ( B 
\  ( B  \  A ) )  =  ( B  i^i  A
)
1211eqeq1i 2461 . 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 1370    e. wcel 1758    \ cdif 3434    i^i cin 3436    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-dif 3440  df-in 3444  df-ss 3451
This theorem is referenced by:  dfin4  3699  sorpsscmpl  6482  sbthlem3  7534  fin23lem7  8597  fin23lem11  8598  compsscnvlem  8651  compssiso  8655  isf34lem4  8658  efgmnvl  16333  frlmlbs  18351  isopn2  18769  iincld  18776  iuncld  18782  clsval2  18787  ntrval2  18788  ntrdif  18789  clsdif  18790  cmclsopn  18799  cmntrcld  18800  opncldf1  18821  indiscld  18828  mretopd  18829  restcld  18909  pnrmopn  19080  conndisj  19153  hausllycmp  19231  kqcldsat  19439  filufint  19626  cfinufil  19634  ufilen  19636  alexsublem  19749  bcth3  20975  inmbl  21157  iccmbl  21181  mbfimaicc  21245  i1fd  21293  itgss3  21426  iundifdifd  26064  iundifdif  26065  cldssbrsiga  26747  kur14lem4  27242  mblfinlem3  28579  mblfinlem4  28580  ismblfin  28581  itg2addnclem  28592  cldbnd  28670  clsun  28672  fdc  28790  frgrawopreg2  30793  lincext2  31122
  Copyright terms: Public domain W3C validator