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

Theorem dfss4 4269
Description: Subclass defined in terms of class difference. See comments under dfun2 4270. (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 4223 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3961 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 320 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 623 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 3967 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 827 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 401 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 623 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 297 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 278 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 4128 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2742 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 278 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  cdif 3948  cin 3950  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-in 3958  df-ss 3968
This theorem is referenced by:  ssdifim  4273  dfin4  4278  sscon34b  4304  sorpsscmpl  7754  sbthlem3  9125  fin23lem7  10356  fin23lem11  10357  compsscnvlem  10410  compssiso  10414  isf34lem4  10417  efgmnvl  19732  frlmlbs  21817  isopn2  23040  iincld  23047  iuncld  23053  clsval2  23058  ntrval2  23059  ntrdif  23060  clsdif  23061  cmclsopn  23070  opncldf1  23092  indiscld  23099  mretopd  23100  restcld  23180  pnrmopn  23351  conndisj  23424  hausllycmp  23502  kqcldsat  23741  filufint  23928  cfinufil  23936  ufilen  23938  alexsublem  24052  bcth3  25365  inmbl  25577  iccmbl  25601  mbfimaicc  25666  i1fd  25716  itgss3  25850  difuncomp  32566  iundifdifd  32574  iundifdif  32575  supppreima  32700  pmtrcnelor  33111  ist0cld  33832  cldssbrsiga  34188  unelcarsg  34314  kur14lem4  35214  cldbnd  36327  clsun  36329  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2addnclem  37678  fdc  37752  dssmapnvod  44033  ntrclsfveq1  44073  ntrclsfveq  44075  ntrclsneine0lem  44077  ntrclsiso  44080  ntrclsk2  44081  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  ntrclsk4  44085  clsneiel2  44122  neicvgel2  44133  salincl  46339  salexct  46349  ovnsubadd2lem  46660  lincext2  48372  opncldeqv  48799
  Copyright terms: Public domain W3C validator