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  6875  0mnnnnn0  9283  nelfzo  10229  fvinim0ffz  10319  wrdlndm  10954  wrdsymb0  10969  rennim  11169  fsumsplitsnun  11586  modfsummodlemstep  11624  sqrt2irr0  12342  isnsgrp  13059  bdnel  15510