Theorem nnel 3044

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2113   ∉ wnel 3034

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 3035

This theorem is referenced by:  raldifsnb  4750  mpoxopynvov0g  8154  fsetexb  8799  0mnnnnn0  12431  ssnn0fi  13906  rabssnn0fi  13907  hashnfinnn0  14282  lcmfunsnlem2lem2  16564  finsumvtxdg2ssteplem1  29568  pthdivtx  29749  wwlksnndef  29927  frgrwopreglem4a  30334  poimirlem26  37786  sticksstones1  42339  afv2orxorb  47416  afv2fv0  47453  lswn0  47632  prminf2  47776