![]() |
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 4680 and eldiftp 4584. (Contributed by Mario Carneiro, 18-Jul-2017.) |
Ref | Expression |
---|---|
eldifpr | ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elprg 4546 | . . . . 5 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) | |
2 | 1 | notbid 321 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ ¬ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) |
3 | neanior 3079 | . . . 4 ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | |
4 | 2, 3 | syl6bbr 292 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))) |
5 | 4 | pm5.32i 578 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))) |
6 | eldif 3891 | . 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶, 𝐷})) | |
7 | 3anass 1092 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))) | |
8 | 5, 6, 7 | 3bitr4i 306 | 1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 ∖ cdif 3878 {cpr 4527 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-ne 2988 df-v 3443 df-dif 3884 df-un 3886 df-sn 4526 df-pr 4528 |
This theorem is referenced by: rexdifpr 4558 logbcl 25353 logbid1 25354 logb1 25355 elogb 25356 logbchbase 25357 relogbval 25358 relogbcl 25359 relogbreexp 25361 relogbmul 25363 relogbexp 25366 nnlogbexp 25367 relogbcxp 25371 cxplogb 25372 relogbcxpb 25373 logbmpt 25374 logbfval 25376 logbgt0b 25379 2logb9irrALT 25384 sqrt2cxp2logb9e3 25385 neldifpr1 30305 neldifpr2 30306 eluz2cnn0n1 44920 rege1logbrege0 44972 relogbmulbexp 44975 relogbdivb 44976 nnpw2blen 44994 |
Copyright terms: Public domain | W3C validator |