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

Theorem dfss4 4060
Description: Subclass defined in terms of class difference. See comments under dfun2 4061. (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 4016 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3779 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 311 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 611 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 3995 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 848 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 390 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 611 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 288 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 269 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 3929 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2811 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 269 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  cdif 3766  cin 3768  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-dif 3772  df-in 3776  df-ss 3783
This theorem is referenced by:  ssdifim  4064  dfin4  4069  sorpsscmpl  7174  sbthlem3  8307  fin23lem7  9419  fin23lem11  9420  compsscnvlem  9473  compssiso  9477  isf34lem4  9480  efgmnvl  18324  frlmlbs  20342  isopn2  21046  iincld  21053  iuncld  21059  clsval2  21064  ntrval2  21065  ntrdif  21066  clsdif  21067  cmclsopn  21076  opncldf1  21098  indiscld  21105  mretopd  21106  restcld  21186  pnrmopn  21357  conndisj  21429  hausllycmp  21507  kqcldsat  21746  filufint  21933  cfinufil  21941  ufilen  21943  alexsublem  22057  bcth3  23336  inmbl  23519  iccmbl  23543  mbfimaicc  23608  i1fd  23658  itgss3  23791  difuncomp  29690  iundifdifd  29701  iundifdif  29702  cldssbrsiga  30571  unelcarsg  30695  kur14lem4  31509  cldbnd  32637  clsun  32639  mblfinlem3  33756  mblfinlem4  33757  ismblfin  33758  itg2addnclem  33768  fdc  33847  dssmapnvod  38808  sscon34b  38811  ntrclsfveq1  38852  ntrclsfveq  38854  ntrclsneine0lem  38856  ntrclsiso  38859  ntrclsk2  38860  ntrclskb  38861  ntrclsk3  38862  ntrclsk13  38863  ntrclsk4  38864  clsneiel2  38901  neicvgel2  38912  salincl  41016  salexct  41025  ovnsubadd2lem  41335  lincext2  42806
  Copyright terms: Public domain W3C validator