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