Theorem eldifpr 4617

Description: Membership in a set with two elements removed. Similar to eldifsn 4744 and eldiftp 4646. (Contributed by Mario Carneiro, 18-Jul-2017.)

Assertion

Ref	Expression
eldifpr	⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))

Proof of Theorem eldifpr

Step	Hyp	Ref	Expression
1		elprg 4605	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)))
2	1	notbid 318	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ ¬ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)))
3		neanior 3026	. . . 4 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
4	2, 3	bitr4di 289	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)))
5	4	pm5.32i 574	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)))
6		eldif 3913	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}))
7		3anass 1095	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)))
8	5, 6, 7	3bitr4i 303	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933   ∖ cdif 3900  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3444  df-dif 3906  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  rexdifpr  4618  logbcl  26750  logbid1  26751  logb1  26752  elogb  26753  logbchbase  26754  relogbval  26755  relogbcl  26756  relogbreexp  26758  relogbmul  26760  relogbexp  26763  nnlogbexp  26764  relogbcxp  26768  cxplogb  26769  relogbcxpb  26770  logbmpt  26771  logbfval  26773  logbgt0b  26776  2logb9irrALT  26781  sqrt2cxp2logb9e3  26782  neldifpr1  32626  neldifpr2  32627  eluz2cnn0n1  48900  rege1logbrege0  48947  relogbmulbexp  48950  relogbdivb  48951  nnpw2blen  48969