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

Theorem dfss4 4185
 Description: Subclass defined in terms of class difference. See comments under dfun2 4186. (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 4142 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3891 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 323 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 625 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 3897 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 825 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 405 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 625 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 300 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 281 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 4052 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2803 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 281 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ∖ cdif 3878   ∩ cin 3880   ⊆ wss 3881 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898 This theorem is referenced by:  ssdifim  4189  dfin4  4194  sscon34b  4219  sorpsscmpl  7442  sbthlem3  8615  fin23lem7  9729  fin23lem11  9730  compsscnvlem  9783  compssiso  9787  isf34lem4  9790  efgmnvl  18835  frlmlbs  20490  isopn2  21644  iincld  21651  iuncld  21657  clsval2  21662  ntrval2  21663  ntrdif  21664  clsdif  21665  cmclsopn  21674  opncldf1  21696  indiscld  21703  mretopd  21704  restcld  21784  pnrmopn  21955  conndisj  22028  hausllycmp  22106  kqcldsat  22345  filufint  22532  cfinufil  22540  ufilen  22542  alexsublem  22656  bcth3  23942  inmbl  24153  iccmbl  24177  mbfimaicc  24242  i1fd  24292  itgss3  24425  difuncomp  30324  iundifdifd  30332  iundifdif  30333  supppreima  30458  pmtrcnelor  30792  ist0cld  31198  cldssbrsiga  31568  unelcarsg  31692  kur14lem4  32581  cldbnd  33799  clsun  33801  mblfinlem3  35112  mblfinlem4  35113  ismblfin  35114  itg2addnclem  35124  fdc  35199  dssmapnvod  40736  ntrclsfveq1  40778  ntrclsfveq  40780  ntrclsneine0lem  40782  ntrclsiso  40785  ntrclsk2  40786  ntrclskb  40787  ntrclsk3  40788  ntrclsk13  40789  ntrclsk4  40790  clsneiel2  40827  neicvgel2  40838  salincl  42980  salexct  42989  ovnsubadd2lem  43299  lincext2  44878
 Copyright terms: Public domain W3C validator