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 ( 𝜑𝐴𝐵 )
nelprd.2 ( 𝜑𝐴𝐶 )
Assertion nelprd ( 𝜑 → ¬ 𝐴 ∈ { 𝐵 , 𝐶 } )

Proof

Step Hyp Ref Expression
1 nelprd.1 ( 𝜑𝐴𝐵 )
2 nelprd.2 ( 𝜑𝐴𝐶 )
3 neanior ( ( 𝐴𝐵𝐴𝐶 ) ↔ ¬ ( 𝐴 = 𝐵𝐴 = 𝐶 ) )
4 elpri ( 𝐴 ∈ { 𝐵 , 𝐶 } → ( 𝐴 = 𝐵𝐴 = 𝐶 ) )
5 4 con3i ( ¬ ( 𝐴 = 𝐵𝐴 = 𝐶 ) → ¬ 𝐴 ∈ { 𝐵 , 𝐶 } )
6 3 5 sylbi ( ( 𝐴𝐵𝐴𝐶 ) → ¬ 𝐴 ∈ { 𝐵 , 𝐶 } )
7 1 2 6 syl2anc ( 𝜑 → ¬ 𝐴 ∈ { 𝐵 , 𝐶 } )