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

Theorem dfss4 4161
Description: Subclass defined in terms of class difference. See comments under dfun2 4162. (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 4118 . 2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
2 eldif 3875 . . . . . . 7 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
32notbii 321 . . . . . 6 𝑥 ∈ (𝐵𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
43anbi2i 622 . . . . 5 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
5 elin 4096 . . . . . 6 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
6 abai 824 . . . . . 6 ((𝑥𝐵𝑥𝐴) ↔ (𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)))
7 iman 402 . . . . . . 7 ((𝑥𝐵𝑥𝐴) ↔ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
87anbi2i 622 . . . . . 6 ((𝑥𝐵 ∧ (𝑥𝐵𝑥𝐴)) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
95, 6, 83bitri 298 . . . . 5 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ (𝑥𝐵 ∧ ¬ 𝑥𝐴)))
104, 9bitr4i 279 . . . 4 ((𝑥𝐵 ∧ ¬ 𝑥 ∈ (𝐵𝐴)) ↔ 𝑥 ∈ (𝐵𝐴))
1110difeqri 4028 . . 3 (𝐵 ∖ (𝐵𝐴)) = (𝐵𝐴)
1211eqeq1i 2802 . 2 ((𝐵 ∖ (𝐵𝐴)) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
131, 12bitr4i 279 1 (𝐴𝐵 ↔ (𝐵 ∖ (𝐵𝐴)) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1525  wcel 2083  cdif 3862  cin 3864  wss 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-v 3442  df-dif 3868  df-in 3872  df-ss 3880
This theorem is referenced by:  ssdifim  4165  dfin4  4170  sorpsscmpl  7325  sbthlem3  8483  fin23lem7  9591  fin23lem11  9592  compsscnvlem  9645  compssiso  9649  isf34lem4  9652  efgmnvl  18571  frlmlbs  20627  isopn2  21328  iincld  21335  iuncld  21341  clsval2  21346  ntrval2  21347  ntrdif  21348  clsdif  21349  cmclsopn  21358  opncldf1  21380  indiscld  21387  mretopd  21388  restcld  21468  pnrmopn  21639  conndisj  21712  hausllycmp  21790  kqcldsat  22029  filufint  22216  cfinufil  22224  ufilen  22226  alexsublem  22340  bcth3  23621  inmbl  23830  iccmbl  23854  mbfimaicc  23919  i1fd  23969  itgss3  24102  difuncomp  29990  iundifdifd  29999  iundifdif  30000  pmtrcnelor  30390  cldssbrsiga  31059  unelcarsg  31183  kur14lem4  32066  cldbnd  33285  clsun  33287  mblfinlem3  34483  mblfinlem4  34484  ismblfin  34485  itg2addnclem  34495  fdc  34573  dssmapnvod  39872  sscon34b  39875  ntrclsfveq1  39916  ntrclsfveq  39918  ntrclsneine0lem  39920  ntrclsiso  39923  ntrclsk2  39924  ntrclskb  39925  ntrclsk3  39926  ntrclsk13  39927  ntrclsk4  39928  clsneiel2  39965  neicvgel2  39976  salincl  42172  salexct  42181  ovnsubadd2lem  42491  lincext2  44012
  Copyright terms: Public domain W3C validator