Definition df-nel 1631

Description: Define negated membership.

Assertion

Ref	Expression
df-nel	⊢ (A ∉ B ↔ ¬ A ∈ B)

Detailed syntax breakdown of Definition df-nel

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wnel 1629	. 2 wff A ∉ B
4	1, 2	wcel 994	. . 3 wff A ∈ B
5	4	wn 2	. 2 wff ¬ A ∈ B
6	3, 5	wb 144	1 wff (A ∉ B ↔ ¬ A ∈ B)

This definition is referenced by:  neleq1 1688  neleq2 1689  ru 1984  snnex 3100  fiprc 4574  ruv 4744  ruALT 4745  pnfnre 5650  mnfnre 5651  ltxrlt 5654  renepnf 5691  renemnf 5692  xrltnr 5695  pnfnlt 5700  nltmnf 5701  sqr2irr 6930  nthruc 6946  eirr 7599  egt2OLD 7600  elt3OLD 7601  egt2lt3 7602  lpni 11417  compfipin0 11493  fbasfip 11627  filfbas 11628  opnfbas 11629  fbunfip 11631  fgfil 11638  extbas1 11641  filrn 11643  rnelfmlem 11698  fcluscomp 11733  tailfb 11762

Copyright terms: Public domain