Theorem nelpr1

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

	Ref	Expression
Hypotheses	nelpr1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	nelpr1.n	⊢ ( 𝜑 → ¬ 𝐴 ∈ { 𝐵 , 𝐶 } )
Assertion	nelpr1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )

Proof

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