Definition df-nel 2443

Description: Define negated membership. (Contributed by NM, 7-Aug-1994.)

Assertion

Ref	Expression
df-nel	⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)

Detailed syntax breakdown of Definition df-nel

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	wnel 2442	. 2 wff 𝐴 ∉ 𝐵
4	1, 2	wcel 2148	. . 3 wff 𝐴 ∈ 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 ∈ 𝐵
6	3, 5	wb 105	1 wff (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)

This definition is referenced by:  neli  2444  nelir  2445  neleq1  2446  neleq2  2447  nfnel  2449  nfneld  2450  elnelne1  2451  elnelne2  2452  nelcon3d  2453  elnelall  2454  ru  2961  sbcnel12g  3074  raldifb  3275  pwnss  4157  pwnex  4447  ruALT  4548  0nelrel  4670  fiprc  6810  0mnnnnn0  9202  fvinim0ffz  10234  rennim  11002  fsumsplitsnun  11418  modfsummodlemstep  11456  sqrt2irr0  12154  isnsgrp  12742  bdnel  14377