Theorem dfin4 4269

Description: Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.)

Assertion

Ref	Expression
dfin4	⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))

Proof of Theorem dfin4

Step	Hyp	Ref	Expression
1		inss1 4230	. . 3 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
2		dfss4 4260	. . 3 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∩ 𝐵))
3	1, 2	mpbi 229	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∩ 𝐵)
4		difin 4263	. . 3 ⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵)
5	4	difeq2i 4118	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∖ (𝐴 ∖ 𝐵))
6	3, 5	eqtr3i 2756	1 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))

Syntax hints:   = wceq 1534   ∖ cdif 3944   ∩ cin 3946   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-in 3954  df-ss 3964

This theorem is referenced by:  indif  4271  cnvin  6156  imain  6644  resin  6865  elcls  23068  cmmbl  25554  mbfeqalem2  25662  itg1addlem4  25719  itg1addlem4OLD  25720  itg1addlem5  25721  suppovss  32597  inelsiga  33968  inelros  34006  topdifinffinlem  37054  poimirlem9  37330  mblfinlem4  37361  ismblfin  37362  cnambfre  37369  stoweidlem50  45671  saliinclf  45947  sge0fodjrnlem  46037  meadjiunlem  46086  caragendifcl  46135