Theorem nnel 3054

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2106   ∉ wnel 3044

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 3045

This theorem is referenced by:  raldifsnb  4801  mpoxopynvov0g  8238  fsetexb  8903  0mnnnnn0  12556  ssnn0fi  14023  rabssnn0fi  14024  hashnfinnn0  14397  lcmfunsnlem2lem2  16673  finsumvtxdg2ssteplem1  29578  pthdivtx  29762  wwlksnndef  29935  frgrwopreglem4a  30339  poimirlem26  37633  sticksstones1  42128  afv2orxorb  47178  afv2fv0  47215  lswn0  47369  prminf2  47513  uspgrimprop  47811