![]() |
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 2948. (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 3051 | . . 3 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
2 | 1 | bicomi 223 | . 2 ⊢ (¬ 𝐴 ∈ 𝐵 ↔ 𝐴 ∉ 𝐵) |
3 | 2 | con1bii 357 | 1 ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∈ wcel 2107 ∉ wnel 3050 |
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 206 df-nel 3051 |
This theorem is referenced by: raldifsnb 4761 mpoxopynvov0g 8150 fsetexb 8809 0mnnnnn0 12452 ssnn0fi 13897 rabssnn0fi 13898 hashnfinnn0 14268 lcmfunsnlem2lem2 16522 finsumvtxdg2ssteplem1 28535 pthdivtx 28719 wwlksnndef 28892 frgrwopreglem4a 29296 poimirlem26 36133 sticksstones1 40583 afv2orxorb 45534 afv2fv0 45571 lswn0 45710 prminf2 45854 |
Copyright terms: Public domain | W3C validator |