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

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

Proof of Theorem eldifpr
StepHypRef Expression
1 elprg 4564 . . . . 5 (𝐴𝐵 → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶𝐴 = 𝐷)))
21notbid 320 . . . 4 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ ¬ (𝐴 = 𝐶𝐴 = 𝐷)))
3 neanior 3098 . . . 4 ((𝐴𝐶𝐴𝐷) ↔ ¬ (𝐴 = 𝐶𝐴 = 𝐷))
42, 3syl6bbr 291 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴𝐶𝐴𝐷)))
54pm5.32i 577 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}) ↔ (𝐴𝐵 ∧ (𝐴𝐶𝐴𝐷)))
6 eldif 3923 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}))
7 3anass 1091 . 2 ((𝐴𝐵𝐴𝐶𝐴𝐷) ↔ (𝐴𝐵 ∧ (𝐴𝐶𝐴𝐷)))
85, 6, 73bitr4i 305 1 (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴𝐵𝐴𝐶𝐴𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 208  wa 398  wo 843  w3a 1083   = wceq 1537  wcel 2114  wne 3006  cdif 3910  {cpr 4545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-ne 3007  df-v 3475  df-dif 3916  df-un 3918  df-sn 4544  df-pr 4546
This theorem is referenced by:  rexdifpr  4574  logbcl  25332  logbid1  25333  logb1  25334  elogb  25335  logbchbase  25336  relogbval  25337  relogbcl  25338  relogbreexp  25340  relogbmul  25342  relogbexp  25345  nnlogbexp  25346  relogbcxp  25350  cxplogb  25351  relogbcxpb  25352  logbmpt  25353  logbfval  25355  logbgt0b  25358  2logb9irrALT  25363  sqrt2cxp2logb9e3  25364  neldifpr1  30280  neldifpr2  30281  eluz2cnn0n1  44711  rege1logbrege0  44763  relogbmulbexp  44766  relogbdivb  44767  nnpw2blen  44785
  Copyright terms: Public domain W3C validator