Metamath Proof Explorer

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 ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ A ≠ B → A ≠ C ↔ A B ≠ B C

Proof

Step Hyp Ref Expression
1 pr1eqbg ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ A ≠ B → A = C ↔ A B = B C
2 1 necon3bid ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ A ≠ B → A ≠ C ↔ A B ≠ B C