![]() |
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 4789 and eldiftp 4689. (Contributed by Mario Carneiro, 18-Jul-2017.) |
Ref | Expression |
---|---|
eldifpr | ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elprg 4648 | . . . . 5 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) | |
2 | 1 | notbid 317 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ ¬ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) |
3 | neanior 3033 | . . . 4 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | |
4 | 2, 3 | bitr4di 288 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))) |
5 | 4 | pm5.32i 573 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))) |
6 | eldif 3957 | . 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷})) | |
7 | 3anass 1093 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))) | |
8 | 5, 6, 7 | 3bitr4i 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 |