Theorem eqoreldif

Description: An element of a set is either equal to another element of the set or a member of the difference of the set and the singleton containing the other element. (Contributed by AV, 25-Aug-2020) (Proof shortened by JJ, 23-Jul-2021)

	Ref	Expression
Assertion	eqoreldif	$$⊢B\in C\to \left(A\in C\leftrightarrow \left(A=B\vee A\in \left(C\setminus \left\{B\right\}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in C\wedge \neg A=B\right)\to A\in C$$
2		elsni	$$⊢A\in \left\{B\right\}\to A=B$$
3	2	con3i	$$⊢\neg A=B\to \neg A\in \left\{B\right\}$$
4	3	adantl	$$⊢\left(A\in C\wedge \neg A=B\right)\to \neg A\in \left\{B\right\}$$
5	1 4	eldifd	$$⊢\left(A\in C\wedge \neg A=B\right)\to A\in \left(C\setminus \left\{B\right\}\right)$$
6	5	ex	$$⊢A\in C\to \left(\neg A=B\to A\in \left(C\setminus \left\{B\right\}\right)\right)$$
7	6	orrd	$$⊢A\in C\to \left(A=B\vee A\in \left(C\setminus \left\{B\right\}\right)\right)$$
8		eleq1a	$$⊢B\in C\to \left(A=B\to A\in C\right)$$
9		eldifi	$$⊢A\in \left(C\setminus \left\{B\right\}\right)\to A\in C$$
10	9	a1i	$$⊢B\in C\to \left(A\in \left(C\setminus \left\{B\right\}\right)\to A\in C\right)$$
11	8 10	jaod	$$⊢B\in C\to \left(\left(A=B\vee A\in \left(C\setminus \left\{B\right\}\right)\right)\to A\in C\right)$$
12	7 11	impbid2	$$⊢B\in C\to \left(A\in C\leftrightarrow \left(A=B\vee A\in \left(C\setminus \left\{B\right\}\right)\right)\right)$$