Theorem nnel 3047

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2114   ∉ wnel 3037

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 207  df-nel 3038

This theorem is referenced by:  raldifsnb  4754  mpoxopynvov0g  8168  fsetexb  8815  0mnnnnn0  12447  ssnn0fi  13922  rabssnn0fi  13923  hashnfinnn0  14298  lcmfunsnlem2lem2  16580  finsumvtxdg2ssteplem1  29637  pthdivtx  29818  wwlksnndef  29996  frgrwopreglem4a  30403  poimirlem26  37926  sticksstones1  42545  afv2orxorb  47617  afv2fv0  47654  lswn0  47833  prminf2  47977