Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfin4 Structured version   Visualization version   GIF version

Theorem dfin4 4242
 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
StepHypRef Expression
1 inss1 4203 . . 3 (𝐴𝐵) ⊆ 𝐴
2 dfss4 4233 . . 3 ((𝐴𝐵) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴𝐵))
31, 2mpbi 232 . 2 (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴𝐵)
4 difin 4236 . . 3 (𝐴 ∖ (𝐴𝐵)) = (𝐴𝐵)
54difeq2i 4094 . 2 (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴 ∖ (𝐴𝐵))
63, 5eqtr3i 2844 1 (𝐴𝐵) = (𝐴 ∖ (𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:   = wceq 1530   ∖ cdif 3931   ∩ cin 3933   ⊆ wss 3934 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-in 3941  df-ss 3950 This theorem is referenced by:  indif  4244  cnvin  5996  imain  6432  resin  6629  elcls  21673  cmmbl  24127  mbfeqalem2  24235  itg1addlem4  24292  itg1addlem5  24293  suppovss  30418  inelsiga  31382  inelros  31420  topdifinffinlem  34615  poimirlem9  34888  mblfinlem4  34919  ismblfin  34920  cnambfre  34927  stoweidlem50  42320  saliincl  42595  sge0fodjrnlem  42683  meadjiunlem  42732  caragendifcl  42781
 Copyright terms: Public domain W3C validator