Theorem dfin4 4241

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 4200	. . 3 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
2		dfss4 4232	. . 3 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∩ 𝐵))
3	1, 2	mpbi 230	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∩ 𝐵)
4		difin 4235	. . 3 ⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵)
5	4	difeq2i 4086	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∖ (𝐴 ∖ 𝐵))
6	3, 5	eqtr3i 2754	1 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))

Syntax hints:   = wceq 1540   ∖ cdif 3911   ∩ cin 3913   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-in 3921  df-ss 3931

This theorem is referenced by:  indif  4243  cnvin  6117  imain  6601  resin  6822  elcls  22960  cmmbl  25435  mbfeqalem2  25543  itg1addlem4  25600  itg1addlem5  25601  suppovss  32604  inelsiga  34125  inelros  34163  topdifinffinlem  37335  poimirlem9  37623  mblfinlem4  37654  ismblfin  37655  cnambfre  37662  stoweidlem50  46048  saliinclf  46324  sge0fodjrnlem  46414  meadjiunlem  46463  caragendifcl  46512