Theorem nnel 3057

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∈ wcel 2107   ∉ wnel 3047

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 3048

This theorem is referenced by:  raldifsnb  4800  mpoxopynvov0g  8199  fsetexb  8858  0mnnnnn0  12504  ssnn0fi  13950  rabssnn0fi  13951  hashnfinnn0  14321  lcmfunsnlem2lem2  16576  finsumvtxdg2ssteplem1  28802  pthdivtx  28986  wwlksnndef  29159  frgrwopreglem4a  29563  poimirlem26  36514  sticksstones1  40962  afv2orxorb  45936  afv2fv0  45973  lswn0  46112  prminf2  46256