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 2108   ∉ 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  4772  mpoxopynvov0g  8213  fsetexb  8878  0mnnnnn0  12533  ssnn0fi  14003  rabssnn0fi  14004  hashnfinnn0  14379  lcmfunsnlem2lem2  16658  finsumvtxdg2ssteplem1  29525  pthdivtx  29709  wwlksnndef  29887  frgrwopreglem4a  30291  poimirlem26  37670  sticksstones1  42159  afv2orxorb  47257  afv2fv0  47294  lswn0  47458  prminf2  47602