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

Theorem difsn 4723
Description: An element not in a set can be removed without affecting the set. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Assertion
Ref Expression
difsn 𝐴𝐵 → (𝐵 ∖ {𝐴}) = 𝐵)

Proof of Theorem difsn
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eldifsn 4711 . . 3 (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ (𝑥𝐵𝑥𝐴))
2 simpl 483 . . . 4 ((𝑥𝐵𝑥𝐴) → 𝑥𝐵)
3 nelelne 3114 . . . . 5 𝐴𝐵 → (𝑥𝐵𝑥𝐴))
43ancld 551 . . . 4 𝐴𝐵 → (𝑥𝐵 → (𝑥𝐵𝑥𝐴)))
52, 4impbid2 227 . . 3 𝐴𝐵 → ((𝑥𝐵𝑥𝐴) ↔ 𝑥𝐵))
61, 5syl5bb 284 . 2 𝐴𝐵 → (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ 𝑥𝐵))
76eqrdv 2816 1 𝐴𝐵 → (𝐵 ∖ {𝐴}) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1528  wcel 2105  wne 3013  cdif 3930  {csn 4557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-v 3494  df-dif 3936  df-sn 4558
This theorem is referenced by:  difsnb  4731  difsnexi  7472  domdifsn  8588  domunsncan  8605  frfi  8751  infdifsn  9108  dfn2  11898  hashgt23el  13773  clslp  21684  xrge00  30600  lindsadd  34766  lindsenlbs  34768  poimirlem2  34775  poimirlem4  34777  poimirlem6  34779  poimirlem7  34780  poimirlem8  34781  poimirlem19  34792  poimirlem23  34796  supxrmnf2  41583  infxrpnf2  41615  dvmptfprodlem  42105  hoiprodp1  42747
  Copyright terms: Public domain W3C validator