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

Theorem dfss4 3404
Description: Subclass defined in terms of class difference. See comments under dfun2 3405. (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 3389 . 2  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
2 eldif 3163 . . . . . . 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 3359 . . . . . 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 3297 . . 3  |-  ( B 
\  ( B  \  A ) )  =  ( B  i^i  A
)
1211eqeq1i 2291 . 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 3150    i^i cin 3152    C_ wss 3153
This theorem is referenced by:  dfin4  3410  sorpsscmpl  6249  sbthlem3  6968  fin23lem7  7937  fin23lem11  7938  compsscnvlem  7991  compssiso  7995  isf34lem4  7998  efgmnvl  15017  isopn2  16763  iincld  16770  iuncld  16776  clsval2  16781  ntrval2  16782  ntrdif  16783  clsdif  16784  cmclsopn  16793  cmntrcld  16794  opncldf1  16815  indiscld  16822  mretopd  16823  restcld  16897  pnrmopn  17065  conndisj  17136  hausllycmp  17214  kqcldsat  17418  filufint  17609  cfinufil  17617  ufilen  17619  alexsublem  17732  bcth3  18747  inmbl  18893  iccmbl  18917  mbfimaicc  18982  i1fd  19030  itgss3  19163  kur14lem4  23144  cldbnd  25643  clsun  25645  fdc  25854  frlmlbs  26648
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 1867  ax-ext 2265
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 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-dif 3156  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator