Theorem nnel 3050

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∈ wcel 2121   ∉ wnel 3040

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 209  df-nel 3041

This theorem is referenced by:  raldifsnb  4732  mpoxopynvov0g  8158  fsetexb  8805  0mnnnnn0  12464  ssnn0fi  13942  rabssnn0fi  13943  hashnfinnn0  14318  lcmfunsnlem2lem2  16603  finsumvtxdg2ssteplem1  29636  pthdivtx  29817  wwlksnndef  29995  frgrwopreglem4a  30402  poimirlem26  38028  sticksstones1  42646  afv2orxorb  47705  afv2fv0  47742  lswn0  47933  nprmmul1  48016  prminf2  48080