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

Theorem dfin4 4232
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 4193 . . 3 (𝐴𝐵) ⊆ 𝐴
2 dfss4 4223 . . 3 ((𝐴𝐵) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴𝐵))
31, 2mpbi 229 . 2 (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴𝐵)
4 difin 4226 . . 3 (𝐴 ∖ (𝐴𝐵)) = (𝐴𝐵)
54difeq2i 4084 . 2 (𝐴 ∖ (𝐴 ∖ (𝐴𝐵))) = (𝐴 ∖ (𝐴𝐵))
63, 5eqtr3i 2767 1 (𝐴𝐵) = (𝐴 ∖ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cdif 3912  cin 3914  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-in 3922  df-ss 3932
This theorem is referenced by:  indif  4234  cnvin  6102  imain  6591  resin  6811  elcls  22440  cmmbl  24914  mbfeqalem2  25022  itg1addlem4  25079  itg1addlem4OLD  25080  itg1addlem5  25081  suppovss  31640  inelsiga  32774  inelros  32812  topdifinffinlem  35847  poimirlem9  36116  mblfinlem4  36147  ismblfin  36148  cnambfre  36155  stoweidlem50  44365  saliinclf  44641  sge0fodjrnlem  44731  meadjiunlem  44780  caragendifcl  44829
  Copyright terms: Public domain W3C validator