Theorem nnel 3075

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∈ wcel 2147   ∉ wnel 3065

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-nel 3066

This theorem is used by:  raldifsnb  4759  mpoxopynvov0g  8256  fsetexb  8911  0mnnnnn0  12662  ssnn0fi  14152  rabssnn0fi  14153  hashnfinnn0  14529  lcmfunsnlem2lem2  16840  finsumvtxdg2ssteplem1  30153  pthdivtx  30339  wwlksnndef  30521  frgrwopreglem4a  30938  poimirlem26  38755  sticksstones1  43387  afv2orxorb  48501  afv2fv0  48538  lswn0  48729  nprmmul1  48812  prminf2  48876