Metamath Proof Explorer

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 ⊢ A ∈ B C ∧ B ≠ C → A = B ↔ A ≠ C

Proof

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