Theorem nnel 3083

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

Syntax hints:  ¬ wn 3   ↔ wb 198   ∈ wcel 2157   ∉ wnel 3074

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 199  df-nel 3075

This theorem is referenced by:  raldifsnb  4515  mpt2xopynvov0g  7578  0mnnnnn0  11614  ssnn0fi  13039  rabssnn0fi  13040  hashnfinnn0  13402  lcmfunsnlem2lem2  15687  finsumvtxdg2ssteplem1  26795  pthdivtx  26983  wwlksnndef  27185  wwlksnfi  27186  frgrwopreglem4a  27659  poimirlem26  33924  afv2orxorb  42082  afv2fv0  42119  lswn0  42220  prminf2  42282