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

Theorem difin 3823
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 441 . . 3 (¬ (𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
2 anclb 568 . . . . 5 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
3 elin 3758 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43imbi2i 325 . . . . 5 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ (𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
5 iman 439 . . . . 5 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)))
62, 4, 53bitr2i 287 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)))
76con2bii 346 . . 3 ((𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)) ↔ ¬ (𝑥𝐴𝑥𝐵))
8 eldif 3550 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
91, 7, 83bitr4i 291 . 2 ((𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥 ∈ (𝐴𝐵))
109difeqri 3692 1 (𝐴 ∖ (𝐴𝐵)) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1475  wcel 1977  cdif 3537  cin 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547
This theorem is referenced by:  dfin4  3826  indif  3828  dfsymdif3  3852  notrab  3863  disjdif2  3999  dfsdom2  7968  hashdif  13062  isercolllem3  14245  iuncld  20659  llycmpkgen2  21163  1stckgen  21167  txkgen  21265  cmmbl  23109  disjdifprg2  28771  ldgenpisyslem1  29553  onint1  31618  nonrel  36909  nzprmdif  37540
  Copyright terms: Public domain W3C validator