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 224	. 2 ⊢ (¬ 𝐴 ∈ 𝐵 ↔ 𝐴 ∉ 𝐵)
3	2	con1bii 356	1 ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2108   ∉ 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 207  df-nel 3047

This theorem is referenced by:  raldifsnb  4796  mpoxopynvov0g  8239  fsetexb  8904  0mnnnnn0  12558  ssnn0fi  14026  rabssnn0fi  14027  hashnfinnn0  14400  lcmfunsnlem2lem2  16676  finsumvtxdg2ssteplem1  29563  pthdivtx  29747  wwlksnndef  29925  frgrwopreglem4a  30329  poimirlem26  37653  sticksstones1  42147  afv2orxorb  47240  afv2fv0  47277  lswn0  47431  prminf2  47575  uspgrimprop  47873