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

Theorem dfss4 3723
Description: Subclass defined in terms of class difference. See comments under dfun2 3724. (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 3682 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3454 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 308 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 725 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 3662 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 831 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 438 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 725 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 284 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 265 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 3596 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2519 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 265 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1938  cdif 3441  cin 3443  wss 3444
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-v 3079  df-dif 3447  df-in 3451  df-ss 3458
This theorem is referenced by:  dfin4  3729  sorpsscmpl  6721  sbthlem3  7832  fin23lem7  8896  fin23lem11  8897  compsscnvlem  8950  compssiso  8954  isf34lem4  8957  efgmnvl  17856  frlmlbs  19856  isopn2  20547  iincld  20554  iuncld  20560  clsval2  20565  ntrval2  20566  ntrdif  20567  clsdif  20568  cmclsopn  20577  opncldf1  20599  indiscld  20606  mretopd  20607  restcld  20687  pnrmopn  20858  conndisj  20930  hausllycmp  21008  kqcldsat  21247  filufint  21435  cfinufil  21443  ufilen  21445  alexsublem  21559  bcth3  22800  inmbl  22993  iccmbl  23017  mbfimaicc  23082  i1fd  23130  itgss3  23263  frgrawopreg2  26317  difuncomp  28541  iundifdifd  28551  iundifdif  28552  cldssbrsiga  29374  unelcarsg  29508  kur14lem4  30291  cldbnd  31326  clsun  31328  mblfinlem3  32493  mblfinlem4  32494  ismblfin  32495  itg2addnclem  32506  fdc  32586  dssmapnvod  37216  sscon34b  37219  ntrclsfveq1  37260  ntrclsfveq  37262  ntrclsneine0lem  37264  ntrclsiso  37267  ntrclsk2  37268  ntrclskb  37269  ntrclsk3  37270  ntrclsk13  37271  ntrclsk4  37272  clsneiel2  37309  neicvgel2  37320  salincl  39113  salexct  39122  ovnsubadd2lem  39429  frgrwopreg2  41580  lincext2  42130
  Copyright terms: Public domain W3C validator