Theorem nnel 3073

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

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

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 3064

This theorem is used by:  raldifsnb  4763  mpoxopynvov0g  8208  fsetexb  8859  0mnnnnn0  12542  ssnn0fi  14028  rabssnn0fi  14029  hashnfinnn0  14404  lcmfunsnlem2lem2  16703  finsumvtxdg2ssteplem1  29906  pthdivtx  30087  wwlksnndef  30265  frgrwopreglem4a  30672  poimirlem26  38325  sticksstones1  42941  afv2orxorb  47993  afv2fv0  48030  lswn0  48221  nprmmul1  48304  prminf2  48368