Theorem nelprd 4617

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.)

Hypotheses

Ref	Expression
nelprd.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)
nelprd.2	⊢ (𝜑 → 𝐴 ≠ 𝐶)

Assertion

Ref	Expression
nelprd	⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶})

Proof of Theorem nelprd

Step	Hyp	Ref	Expression
1		nelprd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		nelprd.2	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
3		neanior 3048	. . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))
4		elpri 4607	. . . 4 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))
5	4	con3i 155	. . 3 ⊢ (¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶})
6	3, 5	sylbi 220	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶})
7	1, 2, 6	syl2anc 596	1 ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶})

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  {cpr 4585

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-un 4151  df-sn 4584  df-pr 4586

This theorem is used by:  ord2eln012  8505  renfdisj  11369  sumtp  15915  pmtrprfv3  19668  logbgcd1irr  27122  perfectlem2  27557  nbupgrres  29945  usgr2pthlem  30349  eupth2lem3lem6  30834  cycpmco2  33694  cyc2fvx  33695  elrspunsn  33979  esplyind  34207  relogbzexpd  43027  dvrelog2b  43117  dvrelogpow2b  43119  aks4d1p1p4  43122  aks4d1p6  43132  aks6d1c7lem1  43231  mnuprdlem1  45256  mnuprdlem2  45257  perfectALTVlem2  48820