Theorem nnel 2892

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

Syntax hints:  ¬ wn 3   ↔ wb 195   ∈ wcel 1977   ∉ wnel 2781

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 196  df-nel 2783

This theorem is referenced by:  raldifsnb  4266  mpt2xopynvov0g  7227  0mnnnnn0  11202  ssnn0fi  12646  rabssnn0fi  12647  hashnfinnn0  13013  lcmfunsnlem2lem2  15190  nbgranself2  25965  cusgrasizeindslem1  26002  wwlknndef  26265  wwlknfi  26266  clwwlknndef  26301  frgrawopreglem4  26574  poimirlem26  32605  prminf2  40038  lswn0  40242  pthdivtx  40935  wwlksnndef  41111  wwlksnfi  41112  clwwlksnndef  41198  frgrwopreglem4  41484