MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nelprd Structured version   Visualization version   GIF version

Theorem nelprd 4657
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
StepHypRef Expression
1 nelprd.1 . 2 (𝜑𝐴𝐵)
2 nelprd.2 . 2 (𝜑𝐴𝐶)
3 neanior 3035 . . 3 ((𝐴𝐵𝐴𝐶) ↔ ¬ (𝐴 = 𝐵𝐴 = 𝐶))
4 elpri 4649 . . . 4 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵𝐴 = 𝐶))
54con3i 154 . . 3 (¬ (𝐴 = 𝐵𝐴 = 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶})
63, 5sylbi 217 . 2 ((𝐴𝐵𝐴𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶})
71, 2, 6syl2anc 584 1 (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 848   = wceq 1540  wcel 2108  wne 2940  {cpr 4628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629
This theorem is referenced by:  ord2eln012  8535  renfdisj  11321  sumtp  15785  pmtrprfv3  19472  logbgcd1irr  26837  perfectlem2  27274  nbupgrres  29381  usgr2pthlem  29783  eupth2lem3lem6  30252  cycpmco2  33153  cyc2fvx  33154  elrspunsn  33457  relogbzexpd  41976  dvrelog2b  42067  dvrelogpow2b  42069  aks4d1p1p4  42072  aks4d1p6  42082  aks6d1c7lem1  42181  mnuprdlem1  44291  mnuprdlem2  44292  perfectALTVlem2  47709
  Copyright terms: Public domain W3C validator