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  3303  pwnss  4192  pwnex  4484  ruALT  4587  0nelrel  4709  fiprc  6874  0mnnnnn0  9281  nelfzo  10227  fvinim0ffz  10317  wrdlndm  10952  wrdsymb0  10967  rennim  11167  fsumsplitsnun  11584  modfsummodlemstep  11622  sqrt2irr0  12332  isnsgrp  13049  bdnel  15500