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  18626  isnmnd  18641  dprddomprc  19908  dprddomcld  19909  dprdval0prc  19910  dprdsubg  19932  zrninitoringc  20561  rng1nnzr  20660  rng1nfld  20664  islindf4  21723  nfimdetndef  22452  mdetfval1  22453  dfac14  23481  0nelfb  23694  fbun  23703  opnfbas  23705  trfbas2  23706  isfil2  23719  fsubbas  23730  fbasrn  23747  rnelfmlem  23815  tsmsfbas  23991  ustfilxp  24076  metustfbas  24421  iccpnfcnv  24818  zclmncvs  25024  cphsqrtcl2  25062  minveclem3b  25304  2sq2  27320  vtxvalprc  28948  iedgvalprc  28949  umgrnloop2  29049  nbuhgr  29246  nbumgr  29250  uhgrnbgr0nb  29257  nbgr0vtx  29258  nbgr0edglem  29259  nbgr1vtx  29261  nbgrnself  29262  nbgrnself2  29263  nbgrssovtx  29264  nbgrssvwo2  29265  nbupgrres  29267  nbusgrvtxm1  29282  nb3grprlem2  29284  1hevtxdg0  29409  p1evtxdeqlem  29416  rgrx0ndm  29497  wlkreslem  29571  dfpth2  29632  pthdlem2lem  29670  wwlksnfi  29809  clwwlkneq0  29931  clwwlknnn  29935  clwwlknon1nloop  30001  clwwlknon1sn  30002  eupth2lem3lem6  30135  nfrgr2v  30174  1to2vfriswmgr  30181  4cyclusnfrgr  30194  frgrnbnb  30195  frgrncvvdeqlem1  30201  frgrncvvdeqlem7  30207  frgrncvvdeqlem8  30208  frgrncvvdeqlem9  30209  frgrwopreg  30225  frgrregord013  30297  lpni  30382  constrsqrtcl  33742  xrge0iifcnv  33896  0nn0m1nnn0  35073  satf0n0  35338  fmlafvel  35345  fmlaomn0  35350  fmlan0  35351  tailfb  36338  dfac21  43028  dvgrat  44274  cvgdvgrat  44275  rusbcALT  44401  fsetsnprcnex  47029  fsetprcnexALT  47036  aiota0ndef  47071  ndfatafv2nrn  47195  afv2ndefb  47198  dfatafv2rnb  47201  fafv2elrnb  47209  afv2ndeffv0  47234  nelbrnel  47250  nelbrnelim  47251  fvmptrab  47266  readdcnnred  47277  resubcnnred  47278  recnmulnred  47279  cndivrenred  47280  sqrtnegnre  47281  0nelsetpreimafv  47364  spr0nelg  47450  spr0el  47456  prminf2  47562  requad01  47595  0noddALTV  47663  1nevenALTV  47665  2noddALTV  47667  nn0o1gt2ALTV  47668  nn0oALTV  47670  341fppr2  47708  9fppr8  47711  clnbgr0vtx  47809  isubgr3stgrlem3  47940  gpg5nbgrvtx03starlem1  48032  gpg5nbgrvtx03starlem2  48033  gpg5nbgrvtx03starlem3  48034  gpg5nbgrvtx13starlem1  48035  gpg5nbgrvtx13starlem2  48036  gpg5nbgrvtx13starlem3  48037  gpg5nbgrvtx03star  48044  gpg5nbgr3star  48045  lidldomnnring  48197  2zrngnring  48219  cznnring  48223  pgrpgt2nabl  48327  lmod1zrnlvec  48456  lvecpsslmod  48469  suppdm  48472  elbigolo1  48519  ifnmfalse  49725  aacllem  49763