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

Theorem difin 4262
Description: Difference with intersection. Theorem 33 of [Suppes] p. 29. (Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
difin (𝐴 ∖ (𝐴𝐵)) = (𝐴𝐵)

Proof of Theorem difin
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 pm4.61 403 . . 3 (¬ (𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
2 anclb 544 . . . . 5 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
3 elin 3965 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43imbi2i 335 . . . . 5 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ (𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
5 iman 400 . . . . 5 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)))
62, 4, 53bitr2i 298 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)))
76con2bii 356 . . 3 ((𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)) ↔ ¬ (𝑥𝐴𝑥𝐵))
8 eldif 3959 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
91, 7, 83bitr4i 302 . 2 ((𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥 ∈ (𝐴𝐵))
109difeqri 4125 1 (𝐴 ∖ (𝐴𝐵)) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394   = wceq 1539  wcel 2104  cdif 3946  cin 3948
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3952  df-in 3956
This theorem is referenced by:  dfin4  4268  indif  4270  dfsymdif3  4297  notrab  4312  disjdif2  4480  dfsdom2  9100  hashdif  14379  isercolllem3  15619  iuncld  22771  llycmpkgen2  23276  1stckgen  23280  txkgen  23378  cmmbl  25285  indifbi  32023  disjdifprg2  32072  ldgenpisyslem1  33457  onint1  35639  nonrel  42639  nzprmdif  43382
  Copyright terms: Public domain W3C validator