Theorem nnel 3062

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2108   ∉ wnel 3052

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 3053

This theorem is referenced by:  raldifsnb  4821  mpoxopynvov0g  8255  fsetexb  8922  0mnnnnn0  12585  ssnn0fi  14036  rabssnn0fi  14037  hashnfinnn0  14410  lcmfunsnlem2lem2  16686  finsumvtxdg2ssteplem1  29581  pthdivtx  29765  wwlksnndef  29938  frgrwopreglem4a  30342  poimirlem26  37606  sticksstones1  42103  afv2orxorb  47143  afv2fv0  47180  lswn0  47318  prminf2  47462  uspgrimprop  47757