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 ( 𝐴𝑉 → ( ¬ 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴𝐵𝐴𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 elprg ( 𝐴𝑉 → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵𝐴 = 𝐶 ) ) )
2 1 notbid ( 𝐴𝑉 → ( ¬ 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ¬ ( 𝐴 = 𝐵𝐴 = 𝐶 ) ) )
3 neanior ( ( 𝐴𝐵𝐴𝐶 ) ↔ ¬ ( 𝐴 = 𝐵𝐴 = 𝐶 ) )
4 2 3 bitr4di ( 𝐴𝑉 → ( ¬ 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴𝐵𝐴𝐶 ) ) )