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