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

Theorem difsn 4691
 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 4680 . . 3 (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ (𝑥𝐵𝑥𝐴))
2 simpl 486 . . . 4 ((𝑥𝐵𝑥𝐴) → 𝑥𝐵)
3 nelelne 3049 . . . . 5 𝐴𝐵 → (𝑥𝐵𝑥𝐴))
43ancld 554 . . . 4 𝐴𝐵 → (𝑥𝐵 → (𝑥𝐵𝑥𝐴)))
52, 4impbid2 229 . . 3 𝐴𝐵 → ((𝑥𝐵𝑥𝐴) ↔ 𝑥𝐵))
61, 5syl5bb 286 . 2 𝐴𝐵 → (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ 𝑥𝐵))
76eqrdv 2756 1 𝐴𝐵 → (𝐵 ∖ {𝐴}) = 𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951   ∖ cdif 3857  {csn 4525 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ne 2952  df-v 3411  df-dif 3863  df-sn 4526 This theorem is referenced by:  difsnb  4699  difsnexi  7488  domdifsn  8634  domunsncan  8651  frfi  8809  infdifsn  9166  dfn2  11960  hashgt23el  13848  clslp  21862  xrge00  30834  lindsadd  35365  lindsenlbs  35367  poimirlem2  35374  poimirlem4  35376  poimirlem6  35378  poimirlem7  35379  poimirlem8  35380  poimirlem19  35391  poimirlem23  35395  supxrmnf2  42481  infxrpnf2  42513  dvmptfprodlem  42997  hoiprodp1  43638
 Copyright terms: Public domain W3C validator