Theorem nnel 3058

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.)

Assertion

Ref	Expression
nnel	⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵)

Proof of Theorem nnel

Step	Hyp	Ref	Expression
1		df-nel 3050	. . 3 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
2	1	bicomi 223	. 2 ⊢ (¬ 𝐴 ∈ 𝐵 ↔ 𝐴 ∉ 𝐵)
3	2	con1bii 357	1 ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵)

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