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

Theorem dfss4 4257
Description: Subclass defined in terms of class difference. See comments under dfun2 4258. (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 4213 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3954 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 319 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 621 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 3960 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 825 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 400 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 621 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 296 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 277 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 4120 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2730 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 277 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  cdif 3941  cin 3943  wss 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-in 3951  df-ss 3961
This theorem is referenced by:  ssdifim  4261  dfin4  4266  sscon34b  4293  sorpsscmpl  7740  sbthlem3  9110  fin23lem7  10341  fin23lem11  10342  compsscnvlem  10395  compssiso  10399  isf34lem4  10402  efgmnvl  19681  frlmlbs  21748  isopn2  22980  iincld  22987  iuncld  22993  clsval2  22998  ntrval2  22999  ntrdif  23000  clsdif  23001  cmclsopn  23010  opncldf1  23032  indiscld  23039  mretopd  23040  restcld  23120  pnrmopn  23291  conndisj  23364  hausllycmp  23442  kqcldsat  23681  filufint  23868  cfinufil  23876  ufilen  23878  alexsublem  23992  bcth3  25303  inmbl  25515  iccmbl  25539  mbfimaicc  25604  i1fd  25654  itgss3  25788  difuncomp  32423  iundifdifd  32431  iundifdif  32432  supppreima  32553  pmtrcnelor  32904  ist0cld  33562  cldssbrsiga  33934  unelcarsg  34060  kur14lem4  34947  cldbnd  35938  clsun  35940  mblfinlem3  37260  mblfinlem4  37261  ismblfin  37262  itg2addnclem  37272  fdc  37346  dssmapnvod  43589  ntrclsfveq1  43629  ntrclsfveq  43631  ntrclsneine0lem  43633  ntrclsiso  43636  ntrclsk2  43637  ntrclskb  43638  ntrclsk3  43639  ntrclsk13  43640  ntrclsk4  43641  clsneiel2  43678  neicvgel2  43689  salincl  45847  salexct  45857  ovnsubadd2lem  46168  lincext2  47706  opncldeqv  48103
  Copyright terms: Public domain W3C validator