Theorem nelpr2

Description: If a class is not an element of an unordered pair, it is not the second listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	nelpr2.a	|- ( ph -> A e. V )
	nelpr2.n	|- ( ph -> -. A e. { B , C } )
Assertion	nelpr2	|- ( ph -> A =/= C )

Proof

Step	Hyp	Ref	Expression
1		nelpr2.a	|- ( ph -> A e. V )
2		nelpr2.n	|- ( ph -> -. A e. { B , C } )
3		animorr	|- ( ( ph /\ A = C ) -> ( A = B \/ A = C ) )
4		elprg	|- ( A e. V -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )
5	1 4	syl	|- ( ph -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )
6	5	adantr	|- ( ( ph /\ A = C ) -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )
7	3 6	mpbird	|- ( ( ph /\ A = C ) -> A e. { B , C } )
8	2 7	mtand	|- ( ph -> -. A = C )
9	8	neqned	|- ( ph -> A =/= C )