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	⊢ ( ¬ 𝐴 ∈ 𝐵 → ( 𝐵 ∖ { 𝐴 } ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 𝐴 } ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴 ) )
2		simpl	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴 ) → 𝑥 ∈ 𝐵 )
3		nelelne	⊢ ( ¬ 𝐴 ∈ 𝐵 → ( 𝑥 ∈ 𝐵 → 𝑥 ≠ 𝐴 ) )
4	3	ancld	⊢ ( ¬ 𝐴 ∈ 𝐵 → ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴 ) ) )
5	2 4	impbid2	⊢ ( ¬ 𝐴 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 𝐴 ) ↔ 𝑥 ∈ 𝐵 ) )
6	1 5	bitrid	⊢ ( ¬ 𝐴 ∈ 𝐵 → ( 𝑥 ∈ ( 𝐵 ∖ { 𝐴 } ) ↔ 𝑥 ∈ 𝐵 ) )
7	6	eqrdv	⊢ ( ¬ 𝐴 ∈ 𝐵 → ( 𝐵 ∖ { 𝐴 } ) = 𝐵 )