MPE Home 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