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

Theorem dfss4 4005
 Description: Subclass defined in terms of class difference. See comments under dfun2 4006. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
dfss4 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)

Proof of Theorem dfss4
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 sseqin2 3966 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3731 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 309 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 601 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 3945 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 806 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 388 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 601 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 286 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 267 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 3879 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2775 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 267 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1630   ∈ wcel 2144   ∖ cdif 3718   ∩ cin 3720   ⊆ wss 3721 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-dif 3724  df-in 3728  df-ss 3735 This theorem is referenced by:  ssdifim  4009  dfin4  4014  sorpsscmpl  7094  sbthlem3  8227  fin23lem7  9339  fin23lem11  9340  compsscnvlem  9393  compssiso  9397  isf34lem4  9400  efgmnvl  18333  frlmlbs  20352  isopn2  21056  iincld  21063  iuncld  21069  clsval2  21074  ntrval2  21075  ntrdif  21076  clsdif  21077  cmclsopn  21086  opncldf1  21108  indiscld  21115  mretopd  21116  restcld  21196  pnrmopn  21367  conndisj  21439  hausllycmp  21517  kqcldsat  21756  filufint  21943  cfinufil  21951  ufilen  21953  alexsublem  22067  bcth3  23346  inmbl  23529  iccmbl  23553  mbfimaicc  23618  i1fd  23667  itgss3  23800  difuncomp  29701  iundifdifd  29712  iundifdif  29713  cldssbrsiga  30584  unelcarsg  30708  kur14lem4  31523  cldbnd  32652  clsun  32654  mblfinlem3  33774  mblfinlem4  33775  ismblfin  33776  itg2addnclem  33786  fdc  33866  dssmapnvod  38833  sscon34b  38836  ntrclsfveq1  38877  ntrclsfveq  38879  ntrclsneine0lem  38881  ntrclsiso  38884  ntrclsk2  38885  ntrclskb  38886  ntrclsk3  38887  ntrclsk13  38888  ntrclsk4  38889  clsneiel2  38926  neicvgel2  38937  salincl  41054  salexct  41063  ovnsubadd2lem  41373  lincext2  42762
 Copyright terms: Public domain W3C validator