Theorem nnel 3057

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∈ wcel 2108   ∉ wnel 3048

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 206  df-nel 3049

This theorem is referenced by:  raldifsnb  4726  mpoxopynvov0g  8001  fsetexb  8610  0mnnnnn0  12195  ssnn0fi  13633  rabssnn0fi  13634  hashnfinnn0  14004  lcmfunsnlem2lem2  16272  finsumvtxdg2ssteplem1  27815  pthdivtx  27998  wwlksnndef  28171  frgrwopreglem4a  28575  poimirlem26  35730  sticksstones1  40030  afv2orxorb  44607  afv2fv0  44644  lswn0  44784  prminf2  44928