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.

Step	Hyp	Ref	Expression
1		eldifsn 4504	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴))
2		simpl 475	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) → 𝑥 ∈ 𝐵)
3		nelelne 3067	. . . . 5 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → 𝑥 ≠ 𝐴))
4	3	ancld 547	. . . 4 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴)))
5	2, 4	impbid2 218	. . 3 ⊢ (¬ 𝐴 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴) ↔ 𝑥 ∈ 𝐵))
6	1, 5	syl5bb 275	. 2 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝑥 ∈ (𝐵 ∖ {𝐴}) ↔ 𝑥 ∈ 𝐵))
7	6	eqrdv 2795	1 ⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∖ {𝐴}) = 𝐵)

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