Theorem pr1nebg

Description: A (proper) pair is not equal to another (maybe improper) pair containing one element of the first pair if and only if the other element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018)

	Ref	Expression
Assertion	pr1nebg	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ≠ 𝐶 ↔ { 𝐴 , 𝐵 } ≠ { 𝐵 , 𝐶 } ) )

Proof

Step	Hyp	Ref	Expression
1		pr1eqbg	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 = 𝐶 ↔ { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } ) )
2	1	necon3bid	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ≠ 𝐶 ↔ { 𝐴 , 𝐵 } ≠ { 𝐵 , 𝐶 } ) )