Definition df-nel 2460

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

This definition is referenced by:  neli  2461  nelir  2462  neleq1  2463  neleq2  2464  nfnel  2466  nfneld  2467  elnelne1  2468  elnelne2  2469  nelcon3d  2470  elnelall  2471  ru  2984  sbcnel12g  3097  raldifb  3299  pwnss  4188  pwnex  4480  ruALT  4583  0nelrel  4705  fiprc  6869  0mnnnnn0  9272  nelfzo  10218  fvinim0ffz  10308  wrdlndm  10931  wrdsymb0  10946  rennim  11146  fsumsplitsnun  11562  modfsummodlemstep  11600  sqrt2irr0  12302  isnsgrp  12989  bdnel  15346