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  4740  mpoxopynvov0g  8159  fsetexb  8806  0mnnnnn0  12464  ssnn0fi  13942  rabssnn0fi  13943  hashnfinnn0  14318  lcmfunsnlem2lem2  16603  finsumvtxdg2ssteplem1  29633  pthdivtx  29814  wwlksnndef  29992  frgrwopreglem4a  30399  poimirlem26  37985  sticksstones1  42603  afv2orxorb  47692  afv2fv0  47729  lswn0  47920  nprmmul1  48003  prminf2  48067