Theorem nnel 3056

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∈ wcel 2106   ∉ wnel 3046

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 3047

This theorem is referenced by:  raldifsnb  4798  mpoxopynvov0g  8195  fsetexb  8854  0mnnnnn0  12500  ssnn0fi  13946  rabssnn0fi  13947  hashnfinnn0  14317  lcmfunsnlem2lem2  16572  finsumvtxdg2ssteplem1  28791  pthdivtx  28975  wwlksnndef  29148  frgrwopreglem4a  29552  poimirlem26  36502  sticksstones1  40950  afv2orxorb  45922  afv2fv0  45959  lswn0  46098  prminf2  46242