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  3748  ruOLD  3749  ssexnelpss  4075  raldifb  4108  elneldisj  4351  elnelun  4352  sbcnel12g  4373  elpwdifsn  4749  0nelrel  5692  feldmfvelcdm  7040  f1ounsn  7229  snnex  7714  pwnex  7715  ssonprc  7743  resf1extb  7890  opabn1stprc  8016  mpoxneldm  8168  mpoxopoveqd  8177  undefnel  8234  fsetdmprc0  8805  fsetcdmex  8813  fsetexb  8814  fiprc  8993  funsnfsupp  9319  elnel  9540  noinfep  9589  dfac9  10066  fz0  13476  0nelfz1  13480  nelfzo  13601  fvinim0ffz  13723  injresinjlem  13724  ssnn0fi  13926  hashnnn0genn0  14284  hashnemnf  14285  hashinfxadd  14326  wrdlndm  14471  wrdsymb0  14490  pfxnd0  14629  repsundef  14712  repswswrd  14725  rennim  15181  cnpart  15182  sqrtneglem  15208  sqreulem  15302  eqsqrtd  15310  fsumsplitsnun  15697  modfsummods  15735  sqrt2irr0  16195  sumeven  16333  sumodd  16334  lcmfval  16567  lcmfn0val  16569  lcmfcl  16574  lcmfnncl  16575  lcmfeq0b  16576  dvdslcmf  16577  lcmftp  16582  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  ncoprmlnprm  16674  prmgaplem5  17002  prmgaplem6  17003  isnsgrp  18632  isnmnd  18647  dprddomprc  19916  dprddomcld  19917  dprdval0prc  19918  dprdsubg  19940  zrninitoringc  20596  rng1nnzr  20695  rng1nfld  20699  islindf4  21780  nfimdetndef  22509  mdetfval1  22510  dfac14  23538  0nelfb  23751  fbun  23760  opnfbas  23762  trfbas2  23763  isfil2  23776  fsubbas  23787  fbasrn  23804  rnelfmlem  23872  tsmsfbas  24048  ustfilxp  24133  metustfbas  24478  iccpnfcnv  24875  zclmncvs  25081  cphsqrtcl2  25119  minveclem3b  25361  2sq2  27377  vtxvalprc  29025  iedgvalprc  29026  umgrnloop2  29126  nbuhgr  29323  nbumgr  29327  uhgrnbgr0nb  29334  nbgr0vtx  29335  nbgr0edglem  29336  nbgr1vtx  29338  nbgrnself  29339  nbgrnself2  29340  nbgrssovtx  29341  nbgrssvwo2  29342  nbupgrres  29344  nbusgrvtxm1  29359  nb3grprlem2  29361  1hevtxdg0  29486  p1evtxdeqlem  29493  rgrx0ndm  29574  wlkreslem  29648  dfpth2  29709  pthdlem2lem  29747  wwlksnfi  29886  clwwlkneq0  30008  clwwlknnn  30012  clwwlknon1nloop  30078  clwwlknon1sn  30079  eupth2lem3lem6  30212  nfrgr2v  30251  1to2vfriswmgr  30258  4cyclusnfrgr  30271  frgrnbnb  30272  frgrncvvdeqlem1  30278  frgrncvvdeqlem7  30284  frgrncvvdeqlem8  30285  frgrncvvdeqlem9  30286  frgrwopreg  30302  frgrregord013  30374  lpni  30459  constrsqrtcl  33762  xrge0iifcnv  33916  0nn0m1nnn0  35093  satf0n0  35358  fmlafvel  35365  fmlaomn0  35370  fmlan0  35371  tailfb  36358  dfac21  43048  dvgrat  44294  cvgdvgrat  44295  rusbcALT  44421  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  47829  isubgr3stgrlem3  47960  gpg5nbgrvtx03starlem1  48052  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx03starlem3  48054  gpg5nbgrvtx13starlem1  48055  gpg5nbgrvtx13starlem2  48056  gpg5nbgrvtx13starlem3  48057  gpg5nbgrvtx03star  48064  gpg5nbgr3star  48065  lidldomnnring  48217  2zrngnring  48239  cznnring  48243  pgrpgt2nabl  48347  lmod1zrnlvec  48476  lvecpsslmod  48489  suppdm  48492  elbigolo1  48539  ifnmfalse  49745  aacllem  49783