Theorem nnel 3071

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

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

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 3062

This theorem is used by:  raldifsnb  4758  mpoxopynvov0g  8231  fsetexb  8886  0mnnnnn0  12638  ssnn0fi  14128  rabssnn0fi  14129  hashnfinnn0  14505  lcmfunsnlem2lem2  16814  finsumvtxdg2ssteplem1  30126  pthdivtx  30312  wwlksnndef  30494  frgrwopreglem4a  30911  poimirlem26  38565  sticksstones1  43197  afv2orxorb  48298  afv2fv0  48335  lswn0  48526  nprmmul1  48609  prminf2  48673