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

Theorem dfss4 4232
Description: Subclass defined in terms of class difference. See comments under dfun2 4233. (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 4189 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3943 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 321 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 622 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 4166 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 822 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 402 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 622 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 298 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 279 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 4098 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2823 . 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 3930  cin 3932  wss 3933
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 2790
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 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-in 3940  df-ss 3949
This theorem is referenced by:  ssdifim  4236  dfin4  4241  sorpsscmpl  7449  sbthlem3  8617  fin23lem7  9726  fin23lem11  9727  compsscnvlem  9780  compssiso  9784  isf34lem4  9787  efgmnvl  18769  frlmlbs  20869  isopn2  21568  iincld  21575  iuncld  21581  clsval2  21586  ntrval2  21587  ntrdif  21588  clsdif  21589  cmclsopn  21598  opncldf1  21620  indiscld  21627  mretopd  21628  restcld  21708  pnrmopn  21879  conndisj  21952  hausllycmp  22030  kqcldsat  22269  filufint  22456  cfinufil  22464  ufilen  22466  alexsublem  22580  bcth3  23861  inmbl  24070  iccmbl  24094  mbfimaicc  24159  i1fd  24209  itgss3  24342  difuncomp  30232  iundifdifd  30241  iundifdif  30242  pmtrcnelor  30662  cldssbrsiga  31345  unelcarsg  31469  kur14lem4  32353  cldbnd  33571  clsun  33573  mblfinlem3  34812  mblfinlem4  34813  ismblfin  34814  itg2addnclem  34824  fdc  34901  dssmapnvod  40244  sscon34b  40247  ntrclsfveq1  40288  ntrclsfveq  40290  ntrclsneine0lem  40292  ntrclsiso  40295  ntrclsk2  40296  ntrclskb  40297  ntrclsk3  40298  ntrclsk13  40299  ntrclsk4  40300  clsneiel2  40337  neicvgel2  40348  salincl  42485  salexct  42494  ovnsubadd2lem  42804  lincext2  44438
  Copyright terms: Public domain W3C validator