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

Theorem dfss4 3645
Description: Subclass defined in terms of class difference. See comments under dfun2 3646. (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 3619 . 2  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
2 eldif 3382 . . . . . . 7  |-  ( x  e.  ( B  \  A )  <->  ( x  e.  B  /\  -.  x  e.  A ) )
32notbii 302 . . . . . 6  |-  ( -.  x  e.  ( B 
\  A )  <->  -.  (
x  e.  B  /\  -.  x  e.  A
) )
43anbi2i 705 . . . . 5  |-  ( ( x  e.  B  /\  -.  x  e.  ( B  \  A ) )  <-> 
( x  e.  B  /\  -.  ( x  e.  B  /\  -.  x  e.  A ) ) )
5 elin 3585 . . . . . 6  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  x  e.  A ) )
6 abai 809 . . . . . 6  |-  ( ( x  e.  B  /\  x  e.  A )  <->  ( x  e.  B  /\  ( x  e.  B  ->  x  e.  A ) ) )
7 iman 430 . . . . . . 7  |-  ( ( x  e.  B  ->  x  e.  A )  <->  -.  ( x  e.  B  /\  -.  x  e.  A
) )
87anbi2i 705 . . . . . 6  |-  ( ( x  e.  B  /\  ( x  e.  B  ->  x  e.  A ) )  <->  ( x  e.  B  /\  -.  (
x  e.  B  /\  -.  x  e.  A
) ) )
95, 6, 83bitri 279 . . . . 5  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  -.  (
x  e.  B  /\  -.  x  e.  A
) ) )
104, 9bitr4i 260 . . . 4  |-  ( ( x  e.  B  /\  -.  x  e.  ( B  \  A ) )  <-> 
x  e.  ( B  i^i  A ) )
1110difeqri 3521 . . 3  |-  ( B 
\  ( B  \  A ) )  =  ( B  i^i  A
)
1211eqeq1i 2457 . 2  |-  ( ( B  \  ( B 
\  A ) )  =  A  <->  ( B  i^i  A )  =  A )
131, 12bitr4i 260 1  |-  ( A 
C_  B  <->  ( B  \  ( B  \  A
) )  =  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1448    e. wcel 1891    \ cdif 3369    i^i cin 3371    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-v 3015  df-dif 3375  df-in 3379  df-ss 3386
This theorem is referenced by:  dfin4  3651  sorpsscmpl  6570  sbthlem3  7671  fin23lem7  8733  fin23lem11  8734  compsscnvlem  8787  compssiso  8791  isf34lem4  8794  efgmnvl  17375  frlmlbs  19366  isopn2  20058  iincld  20065  iuncld  20071  clsval2  20076  ntrval2  20077  ntrdif  20078  clsdif  20079  cmclsopn  20088  cmntrcldOLD  20090  opncldf1  20111  indiscld  20118  mretopd  20119  restcld  20199  pnrmopn  20370  conndisj  20442  hausllycmp  20520  kqcldsat  20759  filufint  20946  cfinufil  20954  ufilen  20956  alexsublem  21070  bcth3  22310  inmbl  22507  iccmbl  22531  mbfimaicc  22601  i1fd  22651  itgss3  22784  frgrawopreg2  25791  difuncomp  28177  iundifdifd  28187  iundifdif  28188  cldssbrsiga  29016  unelcarsg  29150  kur14lem4  29938  cldbnd  30988  clsun  30990  mblfinlem3  31981  mblfinlem4  31982  ismblfin  31983  itg2addnclem  31995  fdc  32076  salincl  38241  salexct  38250  ovnsubadd2lem  38530  lincext2  40573
  Copyright terms: Public domain W3C validator