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 2938. (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 3039 | . . 3 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | |
2 | 1 | bicomi 227 | . 2 ⊢ (¬ 𝐴 ∈ 𝐵 ↔ 𝐴 ∉ 𝐵) |
3 | 2 | con1bii 360 | 1 ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 ∈ wcel 2113 ∉ wnel 3038 |
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 210 df-nel 3039 |
This theorem is referenced by: raldifsnb 4685 mpoxopynvov0g 7910 fsetexb 8475 0mnnnnn0 12009 ssnn0fi 13445 rabssnn0fi 13446 hashnfinnn0 13815 lcmfunsnlem2lem2 16081 finsumvtxdg2ssteplem1 27487 pthdivtx 27670 wwlksnndef 27843 frgrwopreglem4a 28247 poimirlem26 35423 sticksstones1 39705 afv2orxorb 44245 afv2fv0 44282 lswn0 44422 prminf2 44566 |
Copyright terms: Public domain | W3C validator |