Theorem difsnb

Description: ( B \ { A } ) equals B if and only if A is not a member of B . Generalization of difsn . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Assertion	difsnb	$$⊢\neg A\in B\leftrightarrow B\setminus \left\{A\right\}=B$$

Proof

Step	Hyp	Ref	Expression
1		difsn	$$⊢\neg A\in B\to B\setminus \left\{A\right\}=B$$
2		neldifsnd	$$⊢A\in B\to \neg A\in \left(B\setminus \left\{A\right\}\right)$$
3		nelne1	$$⊢\left(A\in B\wedge \neg A\in \left(B\setminus \left\{A\right\}\right)\right)\to B\ne B\setminus \left\{A\right\}$$
4	2 3	mpdan	$$⊢A\in B\to B\ne B\setminus \left\{A\right\}$$
5	4	necomd	$$⊢A\in B\to B\setminus \left\{A\right\}\ne B$$
6	5	necon2bi	$$⊢B\setminus \left\{A\right\}=B\to \neg A\in B$$
7	1 6	impbii	$$⊢\neg A\in B\leftrightarrow B\setminus \left\{A\right\}=B$$