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

Theorem difin 4259
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 406 . . 3 (¬ (𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
2 anclb 547 . . . . 5 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
3 elin 3962 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43imbi2i 336 . . . . 5 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ (𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
5 iman 403 . . . . 5 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)))
62, 4, 53bitr2i 299 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)))
76con2bii 358 . . 3 ((𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)) ↔ ¬ (𝑥𝐴𝑥𝐵))
8 eldif 3956 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
91, 7, 83bitr4i 303 . 2 ((𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥 ∈ (𝐴𝐵))
109difeqri 4122 1 (𝐴 ∖ (𝐴𝐵)) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  wcel 2107  cdif 3943  cin 3945
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 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3949  df-in 3953
This theorem is referenced by:  dfin4  4265  indif  4267  dfsymdif3  4294  notrab  4309  disjdif2  4477  dfsdom2  9091  hashdif  14368  isercolllem3  15608  iuncld  22530  llycmpkgen2  23035  1stckgen  23039  txkgen  23137  cmmbl  25032  indifbi  31735  disjdifprg2  31784  ldgenpisyslem1  33098  onint1  35271  nonrel  42267  nzprmdif  43010
  Copyright terms: Public domain W3C validator