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

Metamath Proof Explorer

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 (A \in C \leftrightarrow (A = B \lor A \in (C ∖ \{B\})))$

Proof

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