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

Theorem difsn 4515
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 4504 . . 3 (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ (𝑥𝐵𝑥𝐴))
2 simpl 475 . . . 4 ((𝑥𝐵𝑥𝐴) → 𝑥𝐵)
3 nelelne 3067 . . . . 5 𝐴𝐵 → (𝑥𝐵𝑥𝐴))
43ancld 547 . . . 4 𝐴𝐵 → (𝑥𝐵 → (𝑥𝐵𝑥𝐴)))
52, 4impbid2 218 . . 3 𝐴𝐵 → ((𝑥𝐵𝑥𝐴) ↔ 𝑥𝐵))
61, 5syl5bb 275 . 2 𝐴𝐵 → (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ 𝑥𝐵))
76eqrdv 2795 1 𝐴𝐵 → (𝐵 ∖ {𝐴}) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 385   = wceq 1653  wcel 2157  wne 2969  cdif 3764  {csn 4366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-v 3385  df-dif 3770  df-sn 4367
This theorem is referenced by:  difsnb  4523  difsnexi  7201  domdifsn  8283  domunsncan  8300  frfi  8445  infdifsn  8802  dfn2  11591  clslp  21278  xrge00  30194  lindsenlbs  33885  poimirlem2  33892  poimirlem4  33894  poimirlem6  33896  poimirlem7  33897  poimirlem8  33898  poimirlem19  33909  poimirlem23  33913  supxrmnf2  40391  infxrpnf2  40424  dvmptfprodlem  40891  hoiprodp1  41536
  Copyright terms: Public domain W3C validator