Theorem difsn 4759

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.

Step	Hyp	Ref	Expression
1		eldifsn 4747	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴))
2		simpl 486	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) → 𝑥 ∈ 𝐵)
3		nelelne 3057	. . . . 5 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → 𝑥 ≠ 𝐴))
4	3	ancld 558	. . . 4 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴)))
5	2, 4	impbid2 228	. . 3 ⊢ (¬ 𝐴 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) ↔ 𝑥 ∈ 𝐵))
6	1, 5	bitrid 285	. 2 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ 𝑥 ∈ 𝐵))
7	6	eqrdv 2761	1 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∖ {𝐴}) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1561   ∈ wcel 2143   ≠ wne 2958   ∖ cdif 3902  {csn 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457  df-dif 3908  df-sn 4584

This theorem is referenced by:  difsnb  4767  difsnexi  7745  domdifsn  9033  domunsncan  9050  frfi  9230  infdifsn  9613  dfn2  12495  hashgt23el  14438  chnccat  18659  clslp  23209  xrge00  33193  lindsadd  38113  lindsenlbs  38115  poimirlem2  38122  poimirlem4  38124  poimirlem6  38126  poimirlem7  38127  poimirlem8  38128  poimirlem19  38139  poimirlem23  38143  supxrmnf2  46008  infxrpnf2  46038  dvmptfprodlem  46519  hoiprodp1  47163