Theorem nnel 3055

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∈ wcel 2105   ∉ wnel 3045

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 3046

This theorem is referenced by:  raldifsnb  4799  mpoxopynvov0g  8205  fsetexb  8864  0mnnnnn0  12511  ssnn0fi  13957  rabssnn0fi  13958  hashnfinnn0  14328  lcmfunsnlem2lem2  16583  finsumvtxdg2ssteplem1  29084  pthdivtx  29268  wwlksnndef  29441  frgrwopreglem4a  29845  poimirlem26  36830  sticksstones1  41281  afv2orxorb  46247  afv2fv0  46284  lswn0  46423  prminf2  46567