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

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

Proof of Theorem eldifpr
StepHypRef Expression
1 elprg 4648 . . . . 5 (𝐴𝐵 → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶𝐴 = 𝐷)))
21notbid 317 . . . 4 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ ¬ (𝐴 = 𝐶𝐴 = 𝐷)))
3 neanior 3033 . . . 4 ((𝐴𝐶𝐴𝐷) ↔ ¬ (𝐴 = 𝐶𝐴 = 𝐷))
42, 3bitr4di 288 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴𝐶𝐴𝐷)))
54pm5.32i 573 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}) ↔ (𝐴𝐵 ∧ (𝐴𝐶𝐴𝐷)))
6 eldif 3957 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}))
7 3anass 1093 . 2 ((𝐴𝐵𝐴𝐶𝐴𝐷) ↔ (𝐴𝐵 ∧ (𝐴𝐶𝐴𝐷)))
85, 6, 73bitr4i 302 1 (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴𝐵𝐴𝐶𝐴𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 394  wo 843  w3a 1085   = wceq 1539  wcel 2104  wne 2938  cdif 3944  {cpr 4629
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-v 3474  df-dif 3950  df-un 3952  df-sn 4628  df-pr 4630
This theorem is referenced by:  rexdifpr  4660  logbcl  26508  logbid1  26509  logb1  26510  elogb  26511  logbchbase  26512  relogbval  26513  relogbcl  26514  relogbreexp  26516  relogbmul  26518  relogbexp  26521  nnlogbexp  26522  relogbcxp  26526  cxplogb  26527  relogbcxpb  26528  logbmpt  26529  logbfval  26531  logbgt0b  26534  2logb9irrALT  26539  sqrt2cxp2logb9e3  26540  neldifpr1  32037  neldifpr2  32038  eluz2cnn0n1  47279  rege1logbrege0  47331  relogbmulbexp  47334  relogbdivb  47335  nnpw2blen  47353
  Copyright terms: Public domain W3C validator