| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nnel | Structured version Visualization version GIF version | ||
| Description: Negation of negated membership, analogous to nne 2944. (Contributed by Alexander van der Vekens, 18-Jan-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
| Ref | Expression |
|---|---|
| nnel | ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-nel 3047 | . . 3 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
| 2 | 1 | bicomi 224 | . 2 ⊢ (¬ 𝐴 ∈ 𝐵 ↔ 𝐴 ∉ 𝐵) |
| 3 | 2 | con1bii 356 | 1 ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 ∈ wcel 2108 ∉ wnel 3046 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-nel 3047 |
| This theorem is referenced by: raldifsnb 4796 mpoxopynvov0g 8239 fsetexb 8904 0mnnnnn0 12558 ssnn0fi 14026 rabssnn0fi 14027 hashnfinnn0 14400 lcmfunsnlem2lem2 16676 finsumvtxdg2ssteplem1 29563 pthdivtx 29747 wwlksnndef 29925 frgrwopreglem4a 30329 poimirlem26 37653 sticksstones1 42147 afv2orxorb 47240 afv2fv0 47277 lswn0 47431 prminf2 47575 uspgrimprop 47873 |
| Copyright terms: Public domain | W3C validator |