Theorem nnel 3073

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∈ wcel 2144   ∉ wnel 3063

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 3064

This theorem is referenced by:  raldifsnb  4758  mpoxopynvov0g  8196  fsetexb  8847  0mnnnnn0  12515  ssnn0fi  14000  rabssnn0fi  14001  hashnfinnn0  14376  lcmfunsnlem2lem2  16675  finsumvtxdg2ssteplem1  29748  pthdivtx  29929  wwlksnndef  30107  frgrwopreglem4a  30514  poimirlem26  38150  sticksstones1  42768  afv2orxorb  47827  afv2fv0  47864  lswn0  48055  nprmmul1  48138  prminf2  48202