Theorem dfss4 4258

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   ∖ cdif 3945   ∩ cin 3947   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-in 3955  df-ss 3965

This theorem is referenced by:  ssdifim  4262  dfin4  4267  sscon34b  4294  sorpsscmpl  7721  sbthlem3  9082  fin23lem7  10308  fin23lem11  10309  compsscnvlem  10362  compssiso  10366  isf34lem4  10369  efgmnvl  19577  frlmlbs  21344  isopn2  22528  iincld  22535  iuncld  22541  clsval2  22546  ntrval2  22547  ntrdif  22548  clsdif  22549  cmclsopn  22558  opncldf1  22580  indiscld  22587  mretopd  22588  restcld  22668  pnrmopn  22839  conndisj  22912  hausllycmp  22990  kqcldsat  23229  filufint  23416  cfinufil  23424  ufilen  23426  alexsublem  23540  bcth3  24840  inmbl  25051  iccmbl  25075  mbfimaicc  25140  i1fd  25190  itgss3  25324  difuncomp  31773  iundifdifd  31781  iundifdif  31782  supppreima  31901  pmtrcnelor  32240  ist0cld  32802  cldssbrsiga  33174  unelcarsg  33300  kur14lem4  34189  cldbnd  35200  clsun  35202  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  itg2addnclem  36528  fdc  36602  dssmapnvod  42757  ntrclsfveq1  42797  ntrclsfveq  42799  ntrclsneine0lem  42801  ntrclsiso  42804  ntrclsk2  42805  ntrclskb  42806  ntrclsk3  42807  ntrclsk13  42808  ntrclsk4  42809  clsneiel2  42846  neicvgel2  42857  salincl  45027  salexct  45037  ovnsubadd2lem  45348  lincext2  47090  opncldeqv  47488