Theorem nnel 3039

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2109   ∉ wnel 3029

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 207  df-nel 3030

This theorem is referenced by:  raldifsnb  4756  mpoxopynvov0g  8170  fsetexb  8814  0mnnnnn0  12450  ssnn0fi  13926  rabssnn0fi  13927  hashnfinnn0  14302  lcmfunsnlem2lem2  16585  finsumvtxdg2ssteplem1  29526  pthdivtx  29707  wwlksnndef  29885  frgrwopreglem4a  30289  poimirlem26  37633  sticksstones1  42127  afv2orxorb  47222  afv2fv0  47259  lswn0  47438  prminf2  47582