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

Theorem dfss4 4173
Description: Subclass defined in terms of class difference. See comments under dfun2 4174. (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 4130 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3876 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 323 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 626 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 3882 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 827 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 405 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 626 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 300 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 281 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 4039 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2742 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 281 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1543  wcel 2110  cdif 3863  cin 3865  wss 3866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-in 3873  df-ss 3883
This theorem is referenced by:  ssdifim  4177  dfin4  4182  sscon34b  4209  sorpsscmpl  7522  sbthlem3  8758  fin23lem7  9930  fin23lem11  9931  compsscnvlem  9984  compssiso  9988  isf34lem4  9991  efgmnvl  19104  frlmlbs  20759  isopn2  21929  iincld  21936  iuncld  21942  clsval2  21947  ntrval2  21948  ntrdif  21949  clsdif  21950  cmclsopn  21959  opncldf1  21981  indiscld  21988  mretopd  21989  restcld  22069  pnrmopn  22240  conndisj  22313  hausllycmp  22391  kqcldsat  22630  filufint  22817  cfinufil  22825  ufilen  22827  alexsublem  22941  bcth3  24228  inmbl  24439  iccmbl  24463  mbfimaicc  24528  i1fd  24578  itgss3  24712  difuncomp  30612  iundifdifd  30620  iundifdif  30621  supppreima  30745  pmtrcnelor  31079  ist0cld  31497  cldssbrsiga  31867  unelcarsg  31991  kur14lem4  32884  cldbnd  34252  clsun  34254  mblfinlem3  35553  mblfinlem4  35554  ismblfin  35555  itg2addnclem  35565  fdc  35640  dssmapnvod  41305  ntrclsfveq1  41347  ntrclsfveq  41349  ntrclsneine0lem  41351  ntrclsiso  41354  ntrclsk2  41355  ntrclskb  41356  ntrclsk3  41357  ntrclsk13  41358  ntrclsk4  41359  clsneiel2  41396  neicvgel2  41407  salincl  43539  salexct  43548  ovnsubadd2lem  43858  lincext2  45469  opncldeqv  45868
  Copyright terms: Public domain W3C validator