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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	nelpr2.n	⊢ ( 𝜑 → ¬ 𝐴 ∈ { 𝐵 , 𝐶 } )
Assertion	nelpr2	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		nelpr2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		nelpr2.n	⊢ ( 𝜑 → ¬ 𝐴 ∈ { 𝐵 , 𝐶 } )
3		animorr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) )
4		elprg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
5	1 4	syl	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
7	3 6	mpbird	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ { 𝐵 , 𝐶 } )
8	2 7	mtand	⊢ ( 𝜑 → ¬ 𝐴 = 𝐶 )
9	8	neqned	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )