Theorem dfss4 4214

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ∖ cdif 3894   ∩ cin 3896   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-in 3904  df-ss 3914

This theorem is referenced by:  ssdifim  4218  dfin4  4223  sscon34b  4249  sorpsscmpl  7662  sbthlem3  8997  fin23lem7  10202  fin23lem11  10203  compsscnvlem  10256  compssiso  10260  isf34lem4  10263  efgmnvl  19621  frlmlbs  21729  isopn2  22942  iincld  22949  iuncld  22955  clsval2  22960  ntrval2  22961  ntrdif  22962  clsdif  22963  cmclsopn  22972  opncldf1  22994  indiscld  23001  mretopd  23002  restcld  23082  pnrmopn  23253  conndisj  23326  hausllycmp  23404  kqcldsat  23643  filufint  23830  cfinufil  23838  ufilen  23840  alexsublem  23954  bcth3  25253  inmbl  25465  iccmbl  25489  mbfimaicc  25554  i1fd  25604  itgss3  25738  difuncomp  32525  iundifdifd  32533  iundifdif  32534  supppreima  32664  pmtrcnelor  33052  ist0cld  33838  cldssbrsiga  34192  unelcarsg  34317  kur14lem4  35245  cldbnd  36360  clsun  36362  mblfinlem3  37699  mblfinlem4  37700  ismblfin  37701  itg2addnclem  37711  fdc  37785  dssmapnvod  44053  ntrclsfveq1  44093  ntrclsfveq  44095  ntrclsneine0lem  44097  ntrclsiso  44100  ntrclsk2  44101  ntrclskb  44102  ntrclsk3  44103  ntrclsk13  44104  ntrclsk4  44105  clsneiel2  44142  neicvgel2  44153  salincl  46362  salexct  46372  ovnsubadd2lem  46683  lincext2  48487  opncldeqv  48933