Theorem nnel 3042

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∈ wcel 2111   ∉ wnel 3032

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 3033

This theorem is referenced by:  raldifsnb  4745  mpoxopynvov0g  8144  fsetexb  8788  0mnnnnn0  12413  ssnn0fi  13892  rabssnn0fi  13893  hashnfinnn0  14268  lcmfunsnlem2lem2  16550  finsumvtxdg2ssteplem1  29524  pthdivtx  29705  wwlksnndef  29883  frgrwopreglem4a  30290  poimirlem26  37696  sticksstones1  42249  afv2orxorb  47338  afv2fv0  47375  lswn0  47554  prminf2  47698