Metamath Proof Explorer

Theorem nelpr

Description: A set A not in a pair is neither element of the pair. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Assertion nelpr ⊢ A ∈ V → ¬ A ∈ B C ↔ A ≠ B ∧ A ≠ C

Proof

Step Hyp Ref Expression
1 elprg ⊢ A ∈ V → A ∈ B C ↔ A = B ∨ A = C
2 1 notbid ⊢ A ∈ V → ¬ A ∈ B C ↔ ¬ A = B ∨ A = C
3 neanior ⊢ A ≠ B ∧ A ≠ C ↔ ¬ A = B ∨ A = C
4 2 3 bitr4di ⊢ A ∈ V → ¬ A ∈ B C ↔ A ≠ B ∧ A ≠ C