Definition df-nel 2463

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

This definition is referenced by:  neli  2464  nelir  2465  neleq1  2466  neleq2  2467  nfnel  2469  nfneld  2470  elnelne1  2471  elnelne2  2472  nelcon3d  2473  elnelall  2474  ru  2988  sbcnel12g  3101  raldifb  3304  pwnss  4193  pwnex  4485  ruALT  4588  0nelrel  4710  fiprc  6883  0mnnnnn0  9300  nelfzo  10246  fvinim0ffz  10336  wrdlndm  10971  wrdsymb0  10986  rennim  11186  fsumsplitsnun  11603  modfsummodlemstep  11641  sqrt2irr0  12359  isnsgrp  13110  bdnel  15608