Theorem nnel 3080

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∈ wcel 2149   ∉ wnel 3070

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 210  df-nel 3071

This theorem is referenced by:  raldifsnb  4765  mpoxopynvov0g  8206  fsetexb  8857  0mnnnnn0  12532  ssnn0fi  14017  rabssnn0fi  14018  hashnfinnn0  14393  lcmfunsnlem2lem2  16693  finsumvtxdg2ssteplem1  29832  pthdivtx  30013  wwlksnndef  30191  frgrwopreglem4a  30598  poimirlem26  38180  sticksstones1  42798  afv2orxorb  47847  afv2fv0  47884  lswn0  48075  nprmmul1  48158  prminf2  48222