Theorem dfss4 4210

Description: Subclass defined in terms of class difference. See comments under dfun2 4211. (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 4164	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)
2		eldif 3900	. . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
3	2	notbii 320	. . . . . 6 ⊢ (¬ 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
4	3	anbi2i 624	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)))
5		elin 3906	. . . . . 6 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
6		abai 827	. . . . . 6 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7		iman 401	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
8	7	anbi2i 624	. . . . . 6 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)))
9	5, 6, 8	3bitri 297	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)))
10	4, 9	bitr4i 278	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴))
11	10	difeqri 4069	. . 3 ⊢ (𝐵 ∖ (𝐵 ∖ 𝐴)) = (𝐵 ∩ 𝐴)
12	11	eqeq1i 2742	. 2 ⊢ ((𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
13	1, 12	bitr4i 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∖ cdif 3887   ∩ cin 3889   ⊆ wss 3890

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-in 3897  df-ss 3907

This theorem is referenced by:  ssdifim  4214  dfin4  4219  sscon34b  4245  sorpsscmpl  7681  sbthlem3  9020  fin23lem7  10229  fin23lem11  10230  compsscnvlem  10283  compssiso  10287  isf34lem4  10290  efgmnvl  19680  frlmlbs  21787  isopn2  23007  iincld  23014  iuncld  23020  clsval2  23025  ntrval2  23026  ntrdif  23027  clsdif  23028  cmclsopn  23037  opncldf1  23059  indiscld  23066  mretopd  23067  restcld  23147  pnrmopn  23318  conndisj  23391  hausllycmp  23469  kqcldsat  23708  filufint  23895  cfinufil  23903  ufilen  23905  alexsublem  24019  bcth3  25308  inmbl  25519  iccmbl  25543  mbfimaicc  25608  i1fd  25658  itgss3  25792  difuncomp  32638  iundifdifd  32646  iundifdif  32647  supppreima  32779  pmtrcnelor  33167  evlextv  33701  ist0cld  33993  cldssbrsiga  34347  unelcarsg  34472  kur14lem4  35407  cldbnd  36524  clsun  36526  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  itg2addnclem  38006  fdc  38080  dssmapnvod  44465  ntrclsfveq1  44505  ntrclsfveq  44507  ntrclsneine0lem  44509  ntrclsiso  44512  ntrclsk2  44513  ntrclskb  44514  ntrclsk3  44515  ntrclsk13  44516  ntrclsk4  44517  clsneiel2  44554  neicvgel2  44565  salincl  46770  salexct  46780  ovnsubadd2lem  47091  lincext2  48943  opncldeqv  49389