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

Theorem difsn 4269
 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 4260 . . 3 (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ (𝑥𝐵𝑥𝐴))
2 simpl 472 . . . 4 ((𝑥𝐵𝑥𝐴) → 𝑥𝐵)
3 nelelne 2880 . . . . 5 𝐴𝐵 → (𝑥𝐵𝑥𝐴))
43ancld 574 . . . 4 𝐴𝐵 → (𝑥𝐵 → (𝑥𝐵𝑥𝐴)))
52, 4impbid2 215 . . 3 𝐴𝐵 → ((𝑥𝐵𝑥𝐴) ↔ 𝑥𝐵))
61, 5syl5bb 271 . 2 𝐴𝐵 → (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ 𝑥𝐵))
76eqrdv 2608 1 𝐴𝐵 → (𝐵 ∖ {𝐴}) = 𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780   ∖ cdif 3537  {csn 4125 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-ne 2782  df-v 3175  df-dif 3543  df-sn 4126 This theorem is referenced by:  difsnb  4278  difsnexi  6864  domdifsn  7928  domunsncan  7945  frfi  8090  infdifsn  8437  dfn2  11182  clslp  20762  nbgrassovt  25964  xrge00  29017  lindsenlbs  32574  poimirlem2  32581  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem19  32598  poimirlem23  32602  dvmptfprodlem  38834  hoiprodp1  39478
 Copyright terms: Public domain W3C validator