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 e. { B , C } /\ B =/= C ) -> ( A = B <-> A =/= C ) )

Proof

Step	Hyp	Ref	Expression
1		elpri	|- ( A e. { 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 e. { B , C } -> ( B =/= C -> ( A = B <-> A =/= C ) ) )
16	15	imp	|- ( ( A e. { B , C } /\ B =/= C ) -> ( A = B <-> A =/= C ) )