Definition df-nel 2474

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 2473	. 2 wff 𝐴 ∉ 𝐵
4	1, 2	wcel 2178	. . 3 wff 𝐴 ∈ 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 ∈ 𝐵
6	3, 5	wb 105	1 wff (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)

This definition is referenced by:  neli  2475  nelir  2476  neleq1  2477  neleq2  2478  nfnel  2480  nfneld  2481  elnelne1  2482  elnelne2  2483  nelcon3d  2484  elnelall  2485  ru  3004  sbcnel12g  3118  raldifb  3321  pwnss  4219  pwnex  4514  ruALT  4617  0nelrel  4739  fiprc  6931  0mnnnnn0  9362  nelfzo  10309  fvinim0ffz  10407  wrdlndm  11048  wrdsymb0  11063  rennim  11428  fsumsplitsnun  11845  modfsummodlemstep  11883  sqrt2irr0  12601  isnsgrp  13353  vtxvalprc  15767  iedgvalprc  15768  umgrnloop2  15855  bdnel  15989