Theorem nnel 3080

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∈ wcel 2149   ∉ wnel 3070

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 210  df-nel 3071

This theorem is referenced by:  raldifsnb  4766  mpoxopynvov0g  8210  fsetexb  8861  0mnnnnn0  12536  ssnn0fi  14021  rabssnn0fi  14022  hashnfinnn0  14397  lcmfunsnlem2lem2  16697  finsumvtxdg2ssteplem1  29836  pthdivtx  30017  wwlksnndef  30195  frgrwopreglem4a  30602  poimirlem26  38220  sticksstones1  42838  afv2orxorb  47889  afv2fv0  47926  lswn0  48117  nprmmul1  48200  prminf2  48264