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

Theorem dfss4 4259
Description: Subclass defined in terms of class difference. See comments under dfun2 4260. (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 4216 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3959 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 320 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 624 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 3965 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 826 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 403 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 624 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 297 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 278 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 4125 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2738 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 278 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  cdif 3946  cin 3948  wss 3949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966
This theorem is referenced by:  ssdifim  4263  dfin4  4268  sscon34b  4295  sorpsscmpl  7724  sbthlem3  9085  fin23lem7  10311  fin23lem11  10312  compsscnvlem  10365  compssiso  10369  isf34lem4  10372  efgmnvl  19582  frlmlbs  21352  isopn2  22536  iincld  22543  iuncld  22549  clsval2  22554  ntrval2  22555  ntrdif  22556  clsdif  22557  cmclsopn  22566  opncldf1  22588  indiscld  22595  mretopd  22596  restcld  22676  pnrmopn  22847  conndisj  22920  hausllycmp  22998  kqcldsat  23237  filufint  23424  cfinufil  23432  ufilen  23434  alexsublem  23548  bcth3  24848  inmbl  25059  iccmbl  25083  mbfimaicc  25148  i1fd  25198  itgss3  25332  difuncomp  31785  iundifdifd  31793  iundifdif  31794  supppreima  31913  pmtrcnelor  32252  ist0cld  32813  cldssbrsiga  33185  unelcarsg  33311  kur14lem4  34200  cldbnd  35211  clsun  35213  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  itg2addnclem  36539  fdc  36613  dssmapnvod  42771  ntrclsfveq1  42811  ntrclsfveq  42813  ntrclsneine0lem  42815  ntrclsiso  42818  ntrclsk2  42819  ntrclskb  42820  ntrclsk3  42821  ntrclsk13  42822  ntrclsk4  42823  clsneiel2  42860  neicvgel2  42871  salincl  45040  salexct  45050  ovnsubadd2lem  45361  lincext2  47136  opncldeqv  47534
  Copyright terms: Public domain W3C validator