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

Theorem dfss4 3842
Description: Subclass defined in terms of class difference. See comments under dfun2 3843. (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 3801 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3570 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 310 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 729 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 3780 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 835 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 440 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 729 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 286 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 267 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 3714 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2626 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 267 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  cdif 3557  cin 3559  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-dif 3563  df-in 3567  df-ss 3574
This theorem is referenced by:  dfin4  3849  sorpsscmpl  6913  sbthlem3  8032  fin23lem7  9098  fin23lem11  9099  compsscnvlem  9152  compssiso  9156  isf34lem4  9159  efgmnvl  18067  frlmlbs  20076  isopn2  20776  iincld  20783  iuncld  20789  clsval2  20794  ntrval2  20795  ntrdif  20796  clsdif  20797  cmclsopn  20806  opncldf1  20828  indiscld  20835  mretopd  20836  restcld  20916  pnrmopn  21087  conndisj  21159  hausllycmp  21237  kqcldsat  21476  filufint  21664  cfinufil  21672  ufilen  21674  alexsublem  21788  bcth3  23068  inmbl  23250  iccmbl  23274  mbfimaicc  23340  i1fd  23388  itgss3  23521  frgrwopreg2  27080  difuncomp  29256  iundifdifd  29266  iundifdif  29267  cldssbrsiga  30073  unelcarsg  30197  kur14lem4  30952  cldbnd  32016  clsun  32018  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  itg2addnclem  33132  fdc  33212  dssmapnvod  37835  sscon34b  37838  ntrclsfveq1  37879  ntrclsfveq  37881  ntrclsneine0lem  37883  ntrclsiso  37886  ntrclsk2  37887  ntrclskb  37888  ntrclsk3  37889  ntrclsk13  37890  ntrclsk4  37891  clsneiel2  37928  neicvgel2  37939  salincl  39880  salexct  39889  ovnsubadd2lem  40196  lincext2  41562
  Copyright terms: Public domain W3C validator