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

Theorem difin 3845
 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 442 . . 3 (¬ (𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
2 anclb 569 . . . . 5 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
3 elin 3780 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43imbi2i 326 . . . . 5 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ (𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
5 iman 440 . . . . 5 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)))
62, 4, 53bitr2i 288 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)))
76con2bii 347 . . 3 ((𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)) ↔ ¬ (𝑥𝐴𝑥𝐵))
8 eldif 3570 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
91, 7, 83bitr4i 292 . 2 ((𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥 ∈ (𝐴𝐵))
109difeqri 3714 1 (𝐴 ∖ (𝐴𝐵)) = (𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ∖ cdif 3557   ∩ cin 3559 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-dif 3563  df-in 3567 This theorem is referenced by:  dfin4  3849  indif  3851  dfsymdif3  3875  notrab  3886  disjdif2  4025  dfsdom2  8043  hashdif  13157  isercolllem3  14347  iuncld  20789  llycmpkgen2  21293  1stckgen  21297  txkgen  21395  cmmbl  23242  disjdifprg2  29275  ldgenpisyslem1  30049  onint1  32143  nonrel  37410  nzprmdif  38039
 Copyright terms: Public domain W3C validator