This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem difsn

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)

		Ref	Expression
	Assertion	difsn	$⊢ \neg A \in B \to B ∖ \{A\} = B$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ x \in (B ∖ \{A\}) \leftrightarrow (x \in B \land x \neq A)$
2		simpl	$⊢ (x \in B \land x \neq A) \to x \in B$
3		nelelne	$⊢ \neg A \in B \to (x \in B \to x \neq A)$
4	3	ancld	$⊢ \neg A \in B \to (x \in B \to (x \in B \land x \neq A))$
5	2 4	impbid2	$⊢ \neg A \in B \to ((x \in B \land x \neq A) \leftrightarrow x \in B)$
6	1 5	bitrid	$⊢ \neg A \in B \to (x \in (B ∖ \{A\}) \leftrightarrow x \in B)$
7	6	eqrdv	$⊢ \neg A \in B \to B ∖ \{A\} = B$