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  4760  mpoxopynvov0g  8193  fsetexb  8837  0mnnnnn0  12474  ssnn0fi  13950  rabssnn0fi  13951  hashnfinnn0  14326  lcmfunsnlem2lem2  16609  finsumvtxdg2ssteplem1  29473  pthdivtx  29657  wwlksnndef  29835  frgrwopreglem4a  30239  poimirlem26  37640  sticksstones1  42134  afv2orxorb  47229  afv2fv0  47266  lswn0  47445  prminf2  47589