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  2985  sbcnel12g  3098  raldifb  3300  pwnss  4189  pwnex  4481  ruALT  4584  0nelrel  4706  fiprc  6871  0mnnnnn0  9275  nelfzo  10221  fvinim0ffz  10311  wrdlndm  10934  wrdsymb0  10949  rennim  11149  fsumsplitsnun  11565  modfsummodlemstep  11603  sqrt2irr0  12305  isnsgrp  12992  bdnel  15416