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  9298  nelfzo  10244  fvinim0ffz  10334  wrdlndm  10969  wrdsymb0  10984  rennim  11184  fsumsplitsnun  11601  modfsummodlemstep  11639  sqrt2irr0  12357  isnsgrp  13108  bdnel  15584