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