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

Theorem dfss4 4234
Description: Subclass defined in terms of class difference. See comments under dfun2 4235. (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 4191 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3945 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 321 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 622 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 4168 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 822 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 402 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 622 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 298 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 279 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 4100 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2826 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 279 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  cdif 3932  cin 3934  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-in 3942  df-ss 3951
This theorem is referenced by:  ssdifim  4238  dfin4  4243  sorpsscmpl  7449  sbthlem3  8618  fin23lem7  9727  fin23lem11  9728  compsscnvlem  9781  compssiso  9785  isf34lem4  9788  efgmnvl  18771  frlmlbs  20871  isopn2  21570  iincld  21577  iuncld  21583  clsval2  21588  ntrval2  21589  ntrdif  21590  clsdif  21591  cmclsopn  21600  opncldf1  21622  indiscld  21629  mretopd  21630  restcld  21710  pnrmopn  21881  conndisj  21954  hausllycmp  22032  kqcldsat  22271  filufint  22458  cfinufil  22466  ufilen  22468  alexsublem  22582  bcth3  23863  inmbl  24072  iccmbl  24096  mbfimaicc  24161  i1fd  24211  itgss3  24344  difuncomp  30233  iundifdifd  30242  iundifdif  30243  pmtrcnelor  30663  cldssbrsiga  31346  unelcarsg  31470  kur14lem4  32354  cldbnd  33572  clsun  33574  mblfinlem3  34813  mblfinlem4  34814  ismblfin  34815  itg2addnclem  34825  fdc  34903  dssmapnvod  40246  sscon34b  40249  ntrclsfveq1  40290  ntrclsfveq  40292  ntrclsneine0lem  40294  ntrclsiso  40297  ntrclsk2  40298  ntrclskb  40299  ntrclsk3  40300  ntrclsk13  40301  ntrclsk4  40302  clsneiel2  40339  neicvgel2  40350  salincl  42489  salexct  42498  ovnsubadd2lem  42808  lincext2  44408
  Copyright terms: Public domain W3C validator