Metamath Proof Explorer

Theorem elprn2

Description: A member of an unordered pair that is not the "second", must be the "first". (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion elprn2 ⊢ A ∈ B C ∧ A ≠ C → A = B

Proof

Step Hyp Ref Expression
1 neneq ⊢ A ≠ C → ¬ A = C
2 1 adantl ⊢ A ∈ B C ∧ A ≠ C → ¬ A = C
3 elpri ⊢ A ∈ B C → A = B ∨ A = C
4 3 adantr ⊢ A ∈ B C ∧ A ≠ C → A = B ∨ A = C
5 orcom ⊢ A = B ∨ A = C ↔ A = C ∨ A = B
6 df-or ⊢ A = C ∨ A = B ↔ ¬ A = C → A = B
7 5 6 bitri ⊢ A = B ∨ A = C ↔ ¬ A = C → A = B
8 4 7 sylib ⊢ A ∈ B C ∧ A ≠ C → ¬ A = C → A = B
9 2 8 mpd ⊢ A ∈ B C ∧ A ≠ C → A = B