Theorem nnel 3040

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2109   ∉ wnel 3030

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 3031

This theorem is referenced by:  raldifsnb  4763  mpoxopynvov0g  8196  fsetexb  8840  0mnnnnn0  12481  ssnn0fi  13957  rabssnn0fi  13958  hashnfinnn0  14333  lcmfunsnlem2lem2  16616  finsumvtxdg2ssteplem1  29480  pthdivtx  29664  wwlksnndef  29842  frgrwopreglem4a  30246  poimirlem26  37647  sticksstones1  42141  afv2orxorb  47233  afv2fv0  47270  lswn0  47449  prminf2  47593