Definition df-nel 3030

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

This definition is referenced by:  neli  3031  nelir  3032  nelcon3d  3033  neleq12d  3034  nfnel  3037  nfneld  3038  nnel  3039  elnelne1  3040  elnelne2  3041  pm2.24nel  3042  pm2.61danel  3043  ru  3740  ruOLD  3741  ssexnelpss  4067  raldifb  4100  elneldisj  4343  elnelun  4344  sbcnel12g  4365  elpwdifsn  4740  0nelrel  5680  feldmfvelcdm  7020  f1ounsn  7209  snnex  7694  pwnex  7695  ssonprc  7723  resf1extb  7867  opabn1stprc  7993  mpoxneldm  8145  mpoxopoveqd  8154  undefnel  8211  fsetdmprc0  8782  fsetcdmex  8790  fsetexb  8791  fiprc  8970  funsnfsupp  9282  elnel  9507  noinfep  9556  dfac9  10031  fz0  13442  0nelfz1  13446  nelfzo  13567  fvinim0ffz  13689  injresinjlem  13690  ssnn0fi  13892  hashnnn0genn0  14250  hashnemnf  14251  hashinfxadd  14292  wrdlndm  14437  wrdsymb0  14456  pfxnd0  14595  repsundef  14677  repswswrd  14690  rennim  15146  cnpart  15147  sqrtneglem  15173  sqreulem  15267  eqsqrtd  15275  fsumsplitsnun  15662  modfsummods  15700  sqrt2irr0  16160  sumeven  16298  sumodd  16299  lcmfval  16532  lcmfn0val  16534  lcmfcl  16539  lcmfnncl  16540  lcmfeq0b  16541  dvdslcmf  16542  lcmftp  16547  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  ncoprmlnprm  16639  prmgaplem5  16967  prmgaplem6  16968  isnsgrp  18597  isnmnd  18612  dprddomprc  19881  dprddomcld  19882  dprdval0prc  19883  dprdsubg  19905  zrninitoringc  20561  rng1nnzr  20660  rng1nfld  20664  islindf4  21745  nfimdetndef  22474  mdetfval1  22475  dfac14  23503  0nelfb  23716  fbun  23725  opnfbas  23727  trfbas2  23728  isfil2  23741  fsubbas  23752  fbasrn  23769  rnelfmlem  23837  tsmsfbas  24013  ustfilxp  24098  metustfbas  24443  iccpnfcnv  24840  zclmncvs  25046  cphsqrtcl2  25084  minveclem3b  25326  2sq2  27342  vtxvalprc  28990  iedgvalprc  28991  umgrnloop2  29091  nbuhgr  29288  nbumgr  29292  uhgrnbgr0nb  29299  nbgr0vtx  29300  nbgr0edglem  29301  nbgr1vtx  29303  nbgrnself  29304  nbgrnself2  29305  nbgrssovtx  29306  nbgrssvwo2  29307  nbupgrres  29309  nbusgrvtxm1  29324  nb3grprlem2  29326  1hevtxdg0  29451  p1evtxdeqlem  29458  rgrx0ndm  29539  wlkreslem  29613  dfpth2  29674  pthdlem2lem  29712  wwlksnfi  29851  clwwlkneq0  29973  clwwlknnn  29977  clwwlknon1nloop  30043  clwwlknon1sn  30044  eupth2lem3lem6  30177  nfrgr2v  30216  1to2vfriswmgr  30223  4cyclusnfrgr  30236  frgrnbnb  30237  frgrncvvdeqlem1  30243  frgrncvvdeqlem7  30249  frgrncvvdeqlem8  30250  frgrncvvdeqlem9  30251  frgrwopreg  30267  frgrregord013  30339  lpni  30424  constrsqrtcl  33752  xrge0iifcnv  33906  0nn0m1nnn0  35096  satf0n0  35361  fmlafvel  35368  fmlaomn0  35373  fmlan0  35374  tailfb  36361  dfac21  43049  dvgrat  44295  cvgdvgrat  44296  rusbcALT  44422  fsetsnprcnex  47049  fsetprcnexALT  47056  aiota0ndef  47091  ndfatafv2nrn  47215  afv2ndefb  47218  dfatafv2rnb  47221  fafv2elrnb  47229  afv2ndeffv0  47254  nelbrnel  47270  nelbrnelim  47271  fvmptrab  47286  readdcnnred  47297  resubcnnred  47298  recnmulnred  47299  cndivrenred  47300  sqrtnegnre  47301  0nelsetpreimafv  47384  spr0nelg  47470  spr0el  47476  prminf2  47582  requad01  47615  0noddALTV  47683  1nevenALTV  47685  2noddALTV  47687  nn0o1gt2ALTV  47688  nn0oALTV  47690  341fppr2  47728  9fppr8  47731  clnbgr0vtx  47830  isubgr3stgrlem3  47962  gpg5nbgrvtx03starlem1  48062  gpg5nbgrvtx03starlem2  48063  gpg5nbgrvtx03starlem3  48064  gpg5nbgrvtx13starlem1  48065  gpg5nbgrvtx13starlem2  48066  gpg5nbgrvtx13starlem3  48067  gpg5nbgrvtx03star  48074  gpg5nbgr3star  48075  lidldomnnring  48230  2zrngnring  48252  cznnring  48256  pgrpgt2nabl  48360  lmod1zrnlvec  48489  lvecpsslmod  48502  suppdm  48505  elbigolo1  48552  ifnmfalse  49758  aacllem  49796