Definition df-nel 3041

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

This definition is referenced by:  neli  3042  nelir  3043  nelcon3d  3044  neleq12d  3045  nfnel  3048  nfneld  3049  nnel  3050  elnelne1  3051  elnelne2  3052  pm2.24nel  3053  pm2.61danel  3054  ru  3722  ruOLD  3723  ssexnelpss  4049  raldifb  4081  elneldisj  4322  elnelun  4323  sbcnel12g  4344  elpwdifsn  4724  0nelrel  5681  feldmfvelcdm  7030  f1ounsn  7219  snnex  7704  pwnex  7705  ssonprc  7733  resf1extb  7878  opabn1stprc  8002  mpoxneldm  8154  mpoxopoveqd  8163  undefnel  8221  fsetdmprc0  8796  fsetcdmex  8804  fsetexb  8805  fiprc  8985  funsnfsupp  9299  elnel  9527  noinfep  9576  dfac9  10054  fz0  13488  0nelfz1  13492  nelfzo  13614  fvinim0ffz  13739  injresinjlem  13740  ssnn0fi  13942  hashnnn0genn0  14300  hashnemnf  14301  hashinfxadd  14342  wrdlndm  14487  wrdsymb0  14506  pfxnd0  14646  repsundef  14728  repswswrd  14741  rennim  15196  cnpart  15197  sqrtneglem  15223  sqreulem  15317  eqsqrtd  15325  fsumsplitsnun  15712  modfsummods  15751  sqrt2irr0  16213  sumeven  16351  sumodd  16352  lcmfval  16585  lcmfn0val  16587  lcmfcl  16592  lcmfnncl  16593  lcmfeq0b  16594  dvdslcmf  16595  lcmftp  16600  lcmfunsnlem2lem1  16602  lcmfunsnlem2lem2  16603  lcmfunsnlem2  16604  ncoprmlnprm  16693  prmgaplem5  17021  prmgaplem6  17022  chnfibg  18597  isnsgrp  18686  isnmnd  18701  dprddomprc  19971  dprddomcld  19972  dprdval0prc  19973  dprdsubg  19995  zrninitoringc  20651  rng1nnzr  20750  rng1nfld  20754  islindf4  21816  nfimdetndef  22575  mdetfval1  22576  dfac14  23604  0nelfb  23817  fbun  23826  opnfbas  23828  trfbas2  23829  isfil2  23842  fsubbas  23853  fbasrn  23870  rnelfmlem  23938  tsmsfbas  24114  ustfilxp  24199  metustfbas  24543  iccpnfcnv  24932  zclmncvs  25136  cphsqrtcl2  25174  minveclem3b  25416  2sq2  27417  vtxvalprc  29134  iedgvalprc  29135  umgrnloop2  29235  nbuhgr  29432  nbumgr  29436  uhgrnbgr0nb  29443  nbgr0vtx  29444  nbgr0edglem  29445  nbgr1vtx  29447  nbgrnself  29448  nbgrnself2  29449  nbgrssovtx  29450  nbgrssvwo2  29451  nbupgrres  29453  nbusgrvtxm1  29468  nb3grprlem2  29470  1hevtxdg0  29594  p1evtxdeqlem  29601  rgrx0ndm  29682  wlkreslem  29756  dfpth2  29817  pthdlem2lem  29855  wwlksnfi  29994  clwwlkneq0  30119  clwwlknnn  30123  clwwlknon1nloop  30189  clwwlknon1sn  30190  eupth2lem3lem6  30323  nfrgr2v  30362  1to2vfriswmgr  30369  4cyclusnfrgr  30382  frgrnbnb  30383  frgrncvvdeqlem1  30389  frgrncvvdeqlem7  30395  frgrncvvdeqlem8  30396  frgrncvvdeqlem9  30397  frgrwopreg  30413  frgrregord013  30485  lpni  30571  evlextv  33736  constrsqrtcl  33973  xrge0iifcnv  34127  noinfepfnregs  35326  noinfepregs  35327  0nn0m1nnn0  35354  satf0n0  35619  fmlafvel  35626  fmlaomn0  35631  fmlan0  35632  tailfb  36618  dfac21  43524  dvgrat  44769  cvgdvgrat  44770  rusbcALT  44895  nthrucw  47343  fsetsnprcnex  47530  fsetprcnexALT  47537  aiota0ndef  47572  ndfatafv2nrn  47696  afv2ndefb  47699  dfatafv2rnb  47702  fafv2elrnb  47710  afv2ndeffv0  47735  nelbrnel  47751  nelbrnelim  47752  fvmptrab  47767  readdcnnred  47778  resubcnnred  47779  recnmulnred  47780  cndivrenred  47781  sqrtnegnre  47782  0nelsetpreimafv  47877  spr0nelg  47963  spr0el  47969  prminf2  48078  indprm  48119  indprmfz  48120  requad01  48124  0noddALTV  48192  1nevenALTV  48194  2noddALTV  48196  nn0o1gt2ALTV  48197  nn0oALTV  48199  341fppr2  48237  9fppr8  48240  clnbgr0vtx  48339  isubgr3stgrlem3  48471  gpg5nbgrvtx03starlem1  48571  gpg5nbgrvtx03starlem2  48572  gpg5nbgrvtx03starlem3  48573  gpg5nbgrvtx13starlem1  48574  gpg5nbgrvtx13starlem2  48575  gpg5nbgrvtx13starlem3  48576  gpg5nbgrvtx03star  48583  gpg5nbgr3star  48584  lidldomnnring  48739  2zrngnring  48761  cznnring  48765  pgrpgt2nabl  48869  lmod1zrnlvec  48997  lvecpsslmod  49010  suppdm  49013  elbigolo1  49060  ifnmfalse  50265  aacllem  50303