Theorem nnel 3134

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∈ wcel 2114   ∉ wnel 3125

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 209  df-nel 3126

This theorem is referenced by:  raldifsnb  4731  mpoxopynvov0g  7882  0mnnnnn0  11932  ssnn0fi  13356  rabssnn0fi  13357  hashnfinnn0  13725  lcmfunsnlem2lem2  15985  finsumvtxdg2ssteplem1  27329  pthdivtx  27512  wwlksnndef  27685  wwlksnfiOLD  27687  frgrwopreglem4a  28091  poimirlem26  34920  afv2orxorb  43434  afv2fv0  43471  lswn0  43611  prminf2  43757