This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → A ∈ V
nelpr1.n ⊢ φ → ¬ A ∈ B C
Assertion nelpr1 ⊢ φ → A ≠ B

Proof

Step Hyp Ref Expression
1 nelpr1.a ⊢ φ → A ∈ V
2 nelpr1.n ⊢ φ → ¬ A ∈ B C
3 animorrl ⊢ φ ∧ A = B → A = B ∨ A = C
4 elprg ⊢ A ∈ V → A ∈ B C ↔ A = B ∨ A = C
5 1 4 syl ⊢ φ → A ∈ B C ↔ A = B ∨ A = C
6 5 adantr ⊢ φ ∧ A = B → A ∈ B C ↔ A = B ∨ A = C
7 3 6 mpbird ⊢ φ ∧ A = B → A ∈ B C
8 2 7 mtand ⊢ φ → ¬ A = B
9 8 neqned ⊢ φ → A ≠ B