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

Theorem dfss4 4274
Description: Subclass defined in terms of class difference. See comments under dfun2 4275. (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 4230 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3972 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 320 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 623 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 3978 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 827 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 401 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 623 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 297 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 278 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 4137 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2739 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 278 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  cdif 3959  cin 3961  wss 3962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-in 3969  df-ss 3979
This theorem is referenced by:  ssdifim  4278  dfin4  4283  sscon34b  4309  sorpsscmpl  7752  sbthlem3  9123  fin23lem7  10353  fin23lem11  10354  compsscnvlem  10407  compssiso  10411  isf34lem4  10414  efgmnvl  19746  frlmlbs  21834  isopn2  23055  iincld  23062  iuncld  23068  clsval2  23073  ntrval2  23074  ntrdif  23075  clsdif  23076  cmclsopn  23085  opncldf1  23107  indiscld  23114  mretopd  23115  restcld  23195  pnrmopn  23366  conndisj  23439  hausllycmp  23517  kqcldsat  23756  filufint  23943  cfinufil  23951  ufilen  23953  alexsublem  24067  bcth3  25378  inmbl  25590  iccmbl  25614  mbfimaicc  25679  i1fd  25729  itgss3  25864  difuncomp  32573  iundifdifd  32581  iundifdif  32582  supppreima  32705  pmtrcnelor  33093  ist0cld  33793  cldssbrsiga  34167  unelcarsg  34293  kur14lem4  35193  cldbnd  36308  clsun  36310  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  itg2addnclem  37657  fdc  37731  dssmapnvod  44009  ntrclsfveq1  44049  ntrclsfveq  44051  ntrclsneine0lem  44053  ntrclsiso  44056  ntrclsk2  44057  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrclsk4  44061  clsneiel2  44098  neicvgel2  44109  salincl  46279  salexct  46289  ovnsubadd2lem  46600  lincext2  48300  opncldeqv  48697
  Copyright terms: Public domain W3C validator