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

Theorem difsn 4730
 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 4718 . . 3 (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ (𝑥𝐵𝑥𝐴))
2 simpl 483 . . . 4 ((𝑥𝐵𝑥𝐴) → 𝑥𝐵)
3 nelelne 3122 . . . . 5 𝐴𝐵 → (𝑥𝐵𝑥𝐴))
43ancld 551 . . . 4 𝐴𝐵 → (𝑥𝐵 → (𝑥𝐵𝑥𝐴)))
52, 4impbid2 227 . . 3 𝐴𝐵 → ((𝑥𝐵𝑥𝐴) ↔ 𝑥𝐵))
61, 5syl5bb 284 . 2 𝐴𝐵 → (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ 𝑥𝐵))
76eqrdv 2824 1 𝐴𝐵 → (𝐵 ∖ {𝐴}) = 𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1530   ∈ wcel 2107   ≠ wne 3021   ∖ cdif 3937  {csn 4564 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-v 3502  df-dif 3943  df-sn 4565 This theorem is referenced by:  difsnb  4738  difsnexi  7472  domdifsn  8589  domunsncan  8606  frfi  8752  infdifsn  9109  dfn2  11899  hashgt23el  13775  clslp  21672  xrge00  30587  lindsadd  34752  lindsenlbs  34754  poimirlem2  34761  poimirlem4  34763  poimirlem6  34765  poimirlem7  34766  poimirlem8  34767  poimirlem19  34778  poimirlem23  34782  supxrmnf2  41572  infxrpnf2  41604  dvmptfprodlem  42094  hoiprodp1  42736
 Copyright terms: Public domain W3C validator