Metamath Proof Explorer


Theorem nelprd

Description: If an element doesn't match the items in an unordered pair, it is not in the unordered pair, deduction version. (Contributed by Alexander van der Vekens, 25-Jan-2018)

Ref Expression
Hypotheses nelprd.1
|- ( ph -> A =/= B )
nelprd.2
|- ( ph -> A =/= C )
Assertion nelprd
|- ( ph -> -. A e. { B , C } )

Proof

Step Hyp Ref Expression
1 nelprd.1
 |-  ( ph -> A =/= B )
2 nelprd.2
 |-  ( ph -> A =/= C )
3 neanior
 |-  ( ( A =/= B /\ A =/= C ) <-> -. ( A = B \/ A = C ) )
4 elpri
 |-  ( A e. { B , C } -> ( A = B \/ A = C ) )
5 4 con3i
 |-  ( -. ( A = B \/ A = C ) -> -. A e. { B , C } )
6 3 5 sylbi
 |-  ( ( A =/= B /\ A =/= C ) -> -. A e. { B , C } )
7 1 2 6 syl2anc
 |-  ( ph -> -. A e. { B , C } )