elprneb

Description: An element of a proper unordered pair is the first element iff it is not the second element. (Contributed by AV, 18-Jun-2020)

		Ref	Expression
	Assertion	elprneb	$⊢ (A \in \{B, C\} \land B \neq C) \to (A = B \leftrightarrow A \neq C)$

Step	Hyp	Ref	Expression
1		elpri	$⊢ A \in \{B, C\} \to (A = B \lor A = C)$
2		neeq1	$⊢ B = A \to (B \neq C \leftrightarrow A \neq C)$
3	2	eqcoms	$⊢ A = B \to (B \neq C \leftrightarrow A \neq C)$
4		pm5.1	$⊢ (A = B \land A \neq C) \to (A = B \leftrightarrow A \neq C)$
5	4	ex	$⊢ A = B \to (A \neq C \to (A = B \leftrightarrow A \neq C))$
6	3 5	sylbid	$⊢ A = B \to (B \neq C \to (A = B \leftrightarrow A \neq C))$
7		neeq2	$⊢ A = C \to (B \neq A \leftrightarrow B \neq C)$
8		nesym	$⊢ B \neq A \leftrightarrow \neg A = B$
9		pm5.1	$⊢ (A = C \land \neg A = B) \to (A = C \leftrightarrow \neg A = B)$
10	8 9	sylan2b	$⊢ (A = C \land B \neq A) \to (A = C \leftrightarrow \neg A = B)$
11	10	necon2abid	$⊢ (A = C \land B \neq A) \to (A = B \leftrightarrow A \neq C)$
12	11	ex	$⊢ A = C \to (B \neq A \to (A = B \leftrightarrow A \neq C))$
13	7 12	sylbird	$⊢ A = C \to (B \neq C \to (A = B \leftrightarrow A \neq C))$
14	6 13	jaoi	$⊢ (A = B \lor A = C) \to (B \neq C \to (A = B \leftrightarrow A \neq C))$
15	1 14	syl	$⊢ A \in \{B, C\} \to (B \neq C \to (A = B \leftrightarrow A \neq C))$
16	15	imp	$⊢ (A \in \{B, C\} \land B \neq C) \to (A = B \leftrightarrow A \neq C)$

Metamath Proof Explorer