Definition df-nel 1857

Description: Define negated membership.

Assertion

Ref	Expression
df-nel	|- (A e/ B <-> -. A e. 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 1855	. 2 wff A e/ B
4	1, 2	wcel 1138	. . 3 wff A e. B
5	4	wn 2	. 2 wff -. A e. B
6	3, 5	wb 162	1 wff (A e/ B <-> -. A e. B)

This definition is referenced by:  neleq1 1935  neleq2 1936  hbnel 1938  ru 2284  snnex 3612  fiprc 5303  undefnel 5370  ruv 5514  ruALT 5515  pnfnre 6461  mnfnre 6462  ltxrlt 6465  renepnf 6504  renepnfOLD 6505  renemnf 6506  renemnfOLD 6507  xrltnr 6512  pnfnlt 6517  nltmnf 6518  sqr2irr 7774  nthruc 7790  eirr 8451  egt2OLD 8452  elt3OLD 8453  egt2lt3 8454  filfbas 10068  fbunfip 10074  fgfil 10082  extbas1 10083  filrn 10085  lpni 10139  bnj24 12180  bnj25OLD 12185  bnj29 12186  1nprm 13561  isprm2 13567  4nprm 13573  compfipin0 15118  fbasfip 15238  opnfbas 15239  rnelfmlem 15274  fcluscomp 15303  tailfb 15321  sbcnel12g 16090  rusbcALT 16092

Copyright terms: Public domain