Theorem nnel 3100

Description: Negation of negated membership, analogous to nne 2991. (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 3092	. . 3 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
2	1	bicomi 227	. 2 ⊢ (¬ 𝐴 ∈ 𝐵 ↔ 𝐴 ∉ 𝐵)
3	2	con1bii 360	1 ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 209   ∈ wcel 2111   ∉ wnel 3091

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 3092

This theorem is referenced by:  raldifsnb  4689  mpoxopynvov0g  7863  0mnnnnn0  11917  ssnn0fi  13348  rabssnn0fi  13349  hashnfinnn0  13718  lcmfunsnlem2lem2  15973  finsumvtxdg2ssteplem1  27335  pthdivtx  27518  wwlksnndef  27691  frgrwopreglem4a  28095  poimirlem26  35083  afv2orxorb  43784  afv2fv0  43821  lswn0  43961  prminf2  44105