Theorem nnel 3046

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

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

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 3037

This theorem is referenced by:  raldifsnb  4741  mpoxopynvov0g  8164  fsetexb  8811  0mnnnnn0  12469  ssnn0fi  13947  rabssnn0fi  13948  hashnfinnn0  14323  lcmfunsnlem2lem2  16608  finsumvtxdg2ssteplem1  29614  pthdivtx  29795  wwlksnndef  29973  frgrwopreglem4a  30380  poimirlem26  37967  sticksstones1  42585  afv2orxorb  47676  afv2fv0  47713  lswn0  47904  nprmmul1  47987  prminf2  48051