![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eldifpr | Structured version Visualization version GIF version |
Description: Membership in a set with two elements removed. Similar to eldifsn 4790 and eldiftp 4691. (Contributed by Mario Carneiro, 18-Jul-2017.) |
Ref | Expression |
---|---|
eldifpr | ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elprg 4652 | . . . . 5 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) | |
2 | 1 | notbid 318 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ ¬ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) |
3 | neanior 3032 | . . . 4 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | |
4 | 2, 3 | bitr4di 289 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))) |
5 | 4 | pm5.32i 574 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))) |
6 | eldif 3972 | . 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷})) | |
7 | 3anass 1094 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))) | |
8 | 5, 6, 7 | 3bitr4i 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 |