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

Theorem eldifpr 4662
Description: Membership in a set with two elements removed. Similar to eldifsn 4790 and eldiftp 4691. (Contributed by Mario Carneiro, 18-Jul-2017.)
Assertion
Ref Expression
eldifpr (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴𝐵𝐴𝐶𝐴𝐷))

Proof of Theorem eldifpr
StepHypRef Expression
1 elprg 4652 . . . . 5 (𝐴𝐵 → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶𝐴 = 𝐷)))
21notbid 318 . . . 4 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ ¬ (𝐴 = 𝐶𝐴 = 𝐷)))
3 neanior 3032 . . . 4 ((𝐴𝐶𝐴𝐷) ↔ ¬ (𝐴 = 𝐶𝐴 = 𝐷))
42, 3bitr4di 289 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴𝐶𝐴𝐷)))
54pm5.32i 574 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}) ↔ (𝐴𝐵 ∧ (𝐴𝐶𝐴𝐷)))
6 eldif 3972 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}))
7 3anass 1094 . 2 ((𝐴𝐵𝐴𝐶𝐴𝐷) ↔ (𝐴𝐵 ∧ (𝐴𝐶𝐴𝐷)))
85, 6, 73bitr4i 303 1 (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴𝐵𝐴𝐶𝐴𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395  wo 847  w3a 1086   = wceq 1536  wcel 2105  wne 2937  cdif 3959  {cpr 4632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-v 3479  df-dif 3965  df-un 3967  df-sn 4631  df-pr 4633
This theorem is referenced by:  rexdifpr  4663  logbcl  26824  logbid1  26825  logb1  26826  elogb  26827  logbchbase  26828  relogbval  26829  relogbcl  26830  relogbreexp  26832  relogbmul  26834  relogbexp  26837  nnlogbexp  26838  relogbcxp  26842  cxplogb  26843  relogbcxpb  26844  logbmpt  26845  logbfval  26847  logbgt0b  26850  2logb9irrALT  26855  sqrt2cxp2logb9e3  26856  neldifpr1  32558  neldifpr2  32559  eluz2cnn0n1  48356  rege1logbrege0  48407  relogbmulbexp  48410  relogbdivb  48411  nnpw2blen  48429
  Copyright terms: Public domain W3C validator