Theorem dfss4 4209

Description: Subclass defined in terms of class difference. See comments under dfun2 4210. (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 4163	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)
2		eldif 3899	. . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
3	2	notbii 320	. . . . . 6 ⊢ (¬ 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
4	3	anbi2i 624	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)))
5		elin 3905	. . . . . 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 4068	. . 3 ⊢ (𝐵 ∖ (𝐵 ∖ 𝐴)) = (𝐵 ∩ 𝐴)
12	11	eqeq1i 2741	. 2 ⊢ ((𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴)
13	1, 12	bitr4i 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴)

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-in 3896  df-ss 3906

This theorem is referenced by:  ssdifim  4213  dfin4  4218  sscon34b  4244  sorpsscmpl  7688  sbthlem3  9027  fin23lem7  10238  fin23lem11  10239  compsscnvlem  10292  compssiso  10296  isf34lem4  10299  efgmnvl  19689  frlmlbs  21777  isopn2  22997  iincld  23004  iuncld  23010  clsval2  23015  ntrval2  23016  ntrdif  23017  clsdif  23018  cmclsopn  23027  opncldf1  23049  indiscld  23056  mretopd  23057  restcld  23137  pnrmopn  23308  conndisj  23381  hausllycmp  23459  kqcldsat  23698  filufint  23885  cfinufil  23893  ufilen  23895  alexsublem  24009  bcth3  25298  inmbl  25509  iccmbl  25533  mbfimaicc  25598  i1fd  25648  itgss3  25782  difuncomp  32623  iundifdifd  32631  iundifdif  32632  supppreima  32764  pmtrcnelor  33152  evlextv  33686  ist0cld  33977  cldssbrsiga  34331  unelcarsg  34456  kur14lem4  35391  cldbnd  36508  clsun  36510  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  itg2addnclem  37992  fdc  38066  dssmapnvod  44447  ntrclsfveq1  44487  ntrclsfveq  44489  ntrclsneine0lem  44491  ntrclsiso  44494  ntrclsk2  44495  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  ntrclsk4  44499  clsneiel2  44536  neicvgel2  44547  salincl  46752  salexct  46762  ovnsubadd2lem  47073  lincext2  48931  opncldeqv  49377