Theorem 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	⊢ ( ( 𝐴 ∈ { 𝐵 , 𝐶 } ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elpri	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } → ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) )
2		neeq1	⊢ ( 𝐵 = 𝐴 → ( 𝐵 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶 ) )
3	2	eqcoms	⊢ ( 𝐴 = 𝐵 → ( 𝐵 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶 ) )
4		pm5.1	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶 ) )
5	4	ex	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≠ 𝐶 → ( 𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶 ) ) )
6	3 5	sylbid	⊢ ( 𝐴 = 𝐵 → ( 𝐵 ≠ 𝐶 → ( 𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶 ) ) )
7		neeq2	⊢ ( 𝐴 = 𝐶 → ( 𝐵 ≠ 𝐴 ↔ 𝐵 ≠ 𝐶 ) )
8		nesym	⊢ ( 𝐵 ≠ 𝐴 ↔ ¬ 𝐴 = 𝐵 )
9		pm5.1	⊢ ( ( 𝐴 = 𝐶 ∧ ¬ 𝐴 = 𝐵 ) → ( 𝐴 = 𝐶 ↔ ¬ 𝐴 = 𝐵 ) )
10	8 9	sylan2b	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 ≠ 𝐴 ) → ( 𝐴 = 𝐶 ↔ ¬ 𝐴 = 𝐵 ) )
11	10	necon2abid	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 ≠ 𝐴 ) → ( 𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶 ) )
12	11	ex	⊢ ( 𝐴 = 𝐶 → ( 𝐵 ≠ 𝐴 → ( 𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶 ) ) )
13	7 12	sylbird	⊢ ( 𝐴 = 𝐶 → ( 𝐵 ≠ 𝐶 → ( 𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶 ) ) )
14	6 13	jaoi	⊢ ( ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) → ( 𝐵 ≠ 𝐶 → ( 𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶 ) ) )
15	1 14	syl	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } → ( 𝐵 ≠ 𝐶 → ( 𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶 ) ) )
16	15	imp	⊢ ( ( 𝐴 ∈ { 𝐵 , 𝐶 } ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶 ) )