Theorem dfss4 4257

Description: Subclass defined in terms of class difference. See comments under dfun2 4258. (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.

Step	Hyp	Ref	Expression
1		sseqin2 4213	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)
2		eldif 3954	. . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
3	2	notbii 319	. . . . . 6 ⊢ (¬ 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
4	3	anbi2i 621	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)))
5		elin 3960	. . . . . 6 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
6		abai 825	. . . . . 6 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7		iman 400	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
8	7	anbi2i 621	. . . . . 6 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)))
9	5, 6, 8	3bitri 296	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)))
10	4, 9	bitr4i 277	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴))
11	10	difeqri 4120	. . 3 ⊢ (𝐵 ∖ (𝐵 ∖ 𝐴)) = (𝐵 ∩ 𝐴)
12	11	eqeq1i 2730	. 2 ⊢ ((𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
13	1, 12	bitr4i 277	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098   ∖ cdif 3941   ∩ cin 3943   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-in 3951  df-ss 3961

This theorem is referenced by:  ssdifim  4261  dfin4  4266  sscon34b  4293  sorpsscmpl  7740  sbthlem3  9110  fin23lem7  10341  fin23lem11  10342  compsscnvlem  10395  compssiso  10399  isf34lem4  10402  efgmnvl  19681  frlmlbs  21748  isopn2  22980  iincld  22987  iuncld  22993  clsval2  22998  ntrval2  22999  ntrdif  23000  clsdif  23001  cmclsopn  23010  opncldf1  23032  indiscld  23039  mretopd  23040  restcld  23120  pnrmopn  23291  conndisj  23364  hausllycmp  23442  kqcldsat  23681  filufint  23868  cfinufil  23876  ufilen  23878  alexsublem  23992  bcth3  25303  inmbl  25515  iccmbl  25539  mbfimaicc  25604  i1fd  25654  itgss3  25788  difuncomp  32423  iundifdifd  32431  iundifdif  32432  supppreima  32553  pmtrcnelor  32904  ist0cld  33562  cldssbrsiga  33934  unelcarsg  34060  kur14lem4  34947  cldbnd  35938  clsun  35940  mblfinlem3  37260  mblfinlem4  37261  ismblfin  37262  itg2addnclem  37272  fdc  37346  dssmapnvod  43589  ntrclsfveq1  43629  ntrclsfveq  43631  ntrclsneine0lem  43633  ntrclsiso  43636  ntrclsk2  43637  ntrclskb  43638  ntrclsk3  43639  ntrclsk13  43640  ntrclsk4  43641  clsneiel2  43678  neicvgel2  43689  salincl  45847  salexct  45857  ovnsubadd2lem  46168  lincext2  47706  opncldeqv  48103