Theorem nelprd 4618

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 3052	. . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))
4		elpri 4608	. . . 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 1570   ∈ wcel 2147   ≠ wne 2959  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  ord2eln012  8530  renfdisj  11393  sumtp  15941  pmtrprfv3  19695  logbgcd1irr  27149  perfectlem2  27584  nbupgrres  29972  usgr2pthlem  30376  eupth2lem3lem6  30861  cycpmco2  33761  cyc2fvx  33762  elrspunsn  34046  esplyind  34274  relogbzexpd  43217  dvrelog2b  43307  dvrelogpow2b  43309  aks4d1p1p4  43312  aks4d1p6  43322  aks6d1c7lem1  43421  mnuprdlem1  45446  mnuprdlem2  45447  perfectALTVlem2  49023