Definition df-nel 2471

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

This definition is referenced by:  neli  2472  nelir  2473  neleq1  2474  neleq2  2475  nfnel  2477  nfneld  2478  elnelne1  2479  elnelne2  2480  nelcon3d  2481  elnelall  2482  ru  2996  sbcnel12g  3109  raldifb  3312  pwnss  4202  pwnex  4495  ruALT  4598  0nelrel  4720  fiprc  6906  0mnnnnn0  9326  nelfzo  10273  fvinim0ffz  10368  wrdlndm  11009  wrdsymb0  11024  rennim  11284  fsumsplitsnun  11701  modfsummodlemstep  11739  sqrt2irr0  12457  isnsgrp  13209  bdnel  15752