Theorem nnel 3047

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

Assertion

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

Proof of Theorem nnel

Step	Hyp	Ref	Expression
1		df-nel 3039	. . 3 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
2	1	bicomi 227	. 2 ⊢ (¬ 𝐴 ∈ 𝐵 ↔ 𝐴 ∉ 𝐵)
3	2	con1bii 360	1 ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵)

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