Theorem nelprd 4631

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 3024	. . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))
4		elpri 4623	. . . 4 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))
5	4	con3i 154	. . 3 ⊢ (¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶})
6	3, 5	sylbi 217	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶})
7	1, 2, 6	syl2anc 584	1 ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶})

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1539   ∈ wcel 2107   ≠ wne 2931  {cpr 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-v 3459  df-un 3929  df-sn 4600  df-pr 4602

This theorem is referenced by:  ord2eln012  8504  renfdisj  11288  sumtp  15754  pmtrprfv3  19422  logbgcd1irr  26742  perfectlem2  27179  nbupgrres  29277  usgr2pthlem  29679  eupth2lem3lem6  30148  cycpmco2  33081  cyc2fvx  33082  elrspunsn  33381  relogbzexpd  41917  dvrelog2b  42008  dvrelogpow2b  42010  aks4d1p1p4  42013  aks4d1p6  42023  aks6d1c7lem1  42122  mnuprdlem1  44229  mnuprdlem2  44230  perfectALTVlem2  47662