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 2113   ∉ 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  4752  mpoxopynvov0g  8156  fsetexb  8803  0mnnnnn0  12435  ssnn0fi  13910  rabssnn0fi  13911  hashnfinnn0  14286  lcmfunsnlem2lem2  16568  finsumvtxdg2ssteplem1  29621  pthdivtx  29802  wwlksnndef  29980  frgrwopreglem4a  30387  poimirlem26  37849  sticksstones1  42422  afv2orxorb  47495  afv2fv0  47532  lswn0  47711  prminf2  47855