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 2145   ∉ 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  4762  mpoxopynvov0g  8215  fsetexb  8868  0mnnnnn0  12563  ssnn0fi  14051  rabssnn0fi  14052  hashnfinnn0  14427  lcmfunsnlem2lem2  16733  finsumvtxdg2ssteplem1  29991  pthdivtx  30177  wwlksnndef  30359  frgrwopreglem4a  30776  poimirlem26  38382  sticksstones1  42999  afv2orxorb  48103  afv2fv0  48140  lswn0  48331  nprmmul1  48414  prminf2  48478