Definition df-nel 2898

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

This definition is referenced by:  neli  2899  nelir  2900  neleq12d  2901  nfnel  2904  nfneld  2905  nnel  2906  elnelne1  2907  elnelne2  2908  nelcon3d  2909  elnelall  2910  pm2.61danel  2911  ru  3434  ssexnelpss  3720  raldifb  3750  elneldisj  3963  elnelun  3964  elneldisjOLD  3965  elnelunOLD  3966  sbcnel12g  3985  elpwdifsn  4319  pwnss  4830  0nelrel  5162  snnex  6966  pwnex  6968  ssonprc  6992  opabn1stprc  7228  mpt2xneldm  7338  mpt2xopoveqd  7347  undefnel  7404  fiprc  8039  funsnfsupp  8299  noinfep  8557  dfac9  8958  fz0  12356  0nelfz1  12360  nelfzo  12475  fvinim0ffz  12587  injresinjlem  12588  ssnn0fi  12784  hashnnn0genn0  13131  hashnemnf  13132  hashinfxadd  13174  ffz0iswrd  13332  wrdsymb0  13339  repsundef  13518  repswswrd  13531  rennim  13979  cnpart  13980  sqrtneglem  14007  sqreulem  14099  eqsqrtd  14107  fsumsplitsnun  14484  fsumsplitsnunOLD  14486  modfsummods  14525  sumeven  15110  sumodd  15111  lcmfval  15334  lcmfn0val  15336  lcmfcl  15341  lcmfnncl  15342  lcmfeq0b  15343  dvdslcmf  15344  lcmftp  15349  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  ncoprmlnprm  15436  prmgaplem5  15759  prmgaplem6  15760  isnsgrp  17288  isnmnd  17298  dprddomprc  18399  dprddomcld  18400  dprdval0prc  18401  dprdsubg  18423  rng1nnzr  19274  rng1nfld  19278  islindf4  20177  nfimdetndef  20395  mdetfval1  20396  dfac14  21421  0nelfb  21635  fbun  21644  opnfbas  21646  trfbas2  21647  isfil2  21660  fsubbas  21671  fbasrn  21688  rnelfmlem  21756  tsmsfbas  21931  ustfilxp  22016  metustfbas  22362  iccpnfcnv  22743  zclmncvs  22948  cphsqrtcl2  22986  minveclem3b  23199  vtxvalprc  25937  iedgvalprc  25938  umgrnloop2  26041  nbuhgr  26239  nbumgr  26243  uhgrnbgr0nb  26250  nbgr0vtxlem  26251  nbgr1vtx  26254  nbgrnself  26257  nbgrnself2  26259  nbgrssovtx  26260  nbgrssvwo2  26261  nbupgrres  26266  nbusgrvtxm1  26281  nb3grprlem2  26283  1hevtxdg0  26401  p1evtxdeqlem  26408  rgrx0ndm  26489  wlkreslem  26566  pthdlem2lem  26663  clwwlksnfi  26913  eupth2lem3lem6  27093  nfrgr2v  27136  1to2vfriswmgr  27143  4cyclusnfrgr  27156  frgrnbnb  27157  frgrncvvdeqlem1  27163  frgrncvvdeqlem7  27169  frgrncvvdeqlem8  27170  frgrncvvdeqlem9  27171  frgrwopreg  27187  frgrregord013  27253  lpni  27332  xrge0iifcnv  29979  tailfb  32372  bj-xpima1sn  32943  bj-xpima1snALT  32944  bj-projval  32984  dfac21  37636  dvgrat  38511  cvgdvgrat  38512  rusbcALT  38640  nelbrnel  41293  nelbrnelim  41294  prminf2  41500  0noddALTV  41600  1nevenALTV  41602  2noddALTV  41604  nn0o1gt2ALTV  41605  nn0oALTV  41607  spr0nelg  41726  spr0el  41732  lidldomnnring  41930  2zrngnring  41952  cznnring  41956  zrninitoringc  42071  pgrpgt2nabl  42147  lmod1zrnlvec  42283  lvecpsslmod  42296  suppdm  42300  elbigolo1  42351  ifnmfalse  42504  aacllem  42547