Theorem dfin4 4244

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

Syntax hints:   = wceq 1540   ∖ cdif 3914   ∩ cin 3916   ⊆ wss 3917

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-in 3924  df-ss 3934

This theorem is referenced by:  indif  4246  cnvin  6120  imain  6604  resin  6825  elcls  22967  cmmbl  25442  mbfeqalem2  25550  itg1addlem4  25607  itg1addlem5  25608  suppovss  32611  inelsiga  34132  inelros  34170  topdifinffinlem  37342  poimirlem9  37630  mblfinlem4  37661  ismblfin  37662  cnambfre  37669  stoweidlem50  46055  saliinclf  46331  sge0fodjrnlem  46421  meadjiunlem  46470  caragendifcl  46519