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

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

Proof of Theorem eldifpr
StepHypRef Expression
1 elprg 4304 . . . . 5 (𝐴𝐵 → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶𝐴 = 𝐷)))
21notbid 307 . . . 4 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ ¬ (𝐴 = 𝐶𝐴 = 𝐷)))
3 neanior 2988 . . . 4 ((𝐴𝐶𝐴𝐷) ↔ ¬ (𝐴 = 𝐶𝐴 = 𝐷))
42, 3syl6bbr 278 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴𝐶𝐴𝐷)))
54pm5.32i 672 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}) ↔ (𝐴𝐵 ∧ (𝐴𝐶𝐴𝐷)))
6 eldif 3690 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}))
7 3anass 1081 . 2 ((𝐴𝐵𝐴𝐶𝐴𝐷) ↔ (𝐴𝐵 ∧ (𝐴𝐶𝐴𝐷)))
85, 6, 73bitr4i 292 1 (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴𝐵𝐴𝐶𝐴𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wo 382  wa 383  w3a 1072   = wceq 1596  wcel 2103  wne 2896  cdif 3677  {cpr 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-v 3306  df-dif 3683  df-un 3685  df-sn 4286  df-pr 4288
This theorem is referenced by:  rexdifpr  4313  logbcl  24625  logbid1  24626  logb1  24627  elogb  24628  logbchbase  24629  relogbval  24630  relogbcl  24631  relogbreexp  24633  relogbmul  24635  relogbexp  24638  nnlogbexp  24639  relogbcxp  24643  cxplogb  24644  relogbcxpb  24645  logbmpt  24646  logbfval  24648  eluz2cnn0n1  42728  rege1logbrege0  42779  relogbmulbexp  42782  relogbdivb  42783  nnpw2blen  42801
  Copyright terms: Public domain W3C validator