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 3020. (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 3124 | . . 3 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
2 | 1 | bicomi 225 | . 2 ⊢ (¬ 𝐴 ∈ 𝐵 ↔ 𝐴 ∉ 𝐵) |
3 | 2 | con1bii 358 | 1 ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 ∈ wcel 2105 ∉ wnel 3123 |
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 208 df-nel 3124 |
This theorem is referenced by: raldifsnb 4723 mpoxopynvov0g 7871 0mnnnnn0 11918 ssnn0fi 13343 rabssnn0fi 13344 hashnfinnn0 13712 lcmfunsnlem2lem2 15973 finsumvtxdg2ssteplem1 27255 pthdivtx 27438 wwlksnndef 27611 wwlksnfiOLD 27613 frgrwopreglem4a 28017 poimirlem26 34800 afv2orxorb 43308 afv2fv0 43345 lswn0 43451 prminf2 43597 |
Copyright terms: Public domain | W3C validator |