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

Theorem nelprd 4622
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 3038 . . 3 ((𝐴𝐵𝐴𝐶) ↔ ¬ (𝐴 = 𝐵𝐴 = 𝐶))
4 elpri 4613 . . . 4 (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵𝐴 = 𝐶))
54con3i 154 . . 3 (¬ (𝐴 = 𝐵𝐴 = 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶})
63, 5sylbi 216 . 2 ((𝐴𝐵𝐴𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶})
71, 2, 6syl2anc 585 1 (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wo 846   = wceq 1542  wcel 2107  wne 2944  {cpr 4593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-v 3450  df-un 3920  df-sn 4592  df-pr 4594
This theorem is referenced by:  ord2eln012  8448  renfdisj  11222  sumtp  15641  pmtrprfv3  19243  logbgcd1irr  26160  perfectlem2  26594  nbupgrres  28354  usgr2pthlem  28753  eupth2lem3lem6  29219  cycpmco2  32024  cyc2fvx  32025  relogbzexpd  40461  dvrelog2b  40552  dvrelogpow2b  40554  aks4d1p1p4  40557  aks4d1p6  40567  mnuprdlem1  42626  mnuprdlem2  42627  perfectALTVlem2  45988
  Copyright terms: Public domain W3C validator