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 2947. (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 3050 | . . 3 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
2 | 1 | bicomi 223 | . 2 ⊢ (¬ 𝐴 ∈ 𝐵 ↔ 𝐴 ∉ 𝐵) |
3 | 2 | con1bii 357 | 1 ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∈ wcel 2106 ∉ wnel 3049 |
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 3050 |
This theorem is referenced by: raldifsnb 4729 mpoxopynvov0g 8030 fsetexb 8652 0mnnnnn0 12265 ssnn0fi 13705 rabssnn0fi 13706 hashnfinnn0 14076 lcmfunsnlem2lem2 16344 finsumvtxdg2ssteplem1 27912 pthdivtx 28097 wwlksnndef 28270 frgrwopreglem4a 28674 poimirlem26 35803 sticksstones1 40102 afv2orxorb 44720 afv2fv0 44757 lswn0 44896 prminf2 45040 |
Copyright terms: Public domain | W3C validator |