Definition df-nel 3066

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

This definition is used by:  neli  3067  nelir  3068  nelcon3d  3069  neleq12d  3070  nfnel  3073  nfneld  3074  nnel  3075  elnelne1  3076  elnelne2  3077  pm2.24nel  3078  pm2.61danel  3079  ru  3741  ssexnelpss  4047  raldifb  4088  elneldisj  4345  elnelun  4346  sbcnel12g  4375  elpwdifsn  4752  0nelrel  5716  feldmfvelcdm  7107  f1ounsn  7300  snnex  7793  pwnex  7794  ssonprc  7822  resf1extb  7967  opabn1stprc  8091  mpoxneldm  8254  mpoxopoveqd  8263  undefnel  8321  fsetdmprc0  8902  fsetcdmex  8910  fsetexb  8911  fiprc  9097  funsnfsupp  9408  elnel  9636  noinfep  9685  dfac9  10239  0nn0m1nnn0  12777  fz0  13696  0nelfz1  13700  nelfzo  13823  fvinim0ffz  13948  injresinjlem  13949  ssnn0fi  14152  hashnnn0genn0  14511  hashnemnf  14512  hashinfxadd  14553  wrdlndm  14699  wrdsymb0  14718  pfxnd0  14863  repsundef  14947  repswswrd  14960  rennim  15432  cnpart  15433  sqrtneglem  15459  sqreulem  15553  eqsqrtd  15561  fsumsplitsnun  15947  modfsummods  15986  sqrt2irr0  16445  sumeven  16583  sumodd  16584  lcmfval  16822  lcmfn0val  16824  lcmfcl  16829  lcmfnncl  16830  lcmfeq0b  16831  dvdslcmf  16832  lcmftp  16837  lcmfunsnlem2lem1  16839  lcmfunsnlem2lem2  16840  lcmfunsnlem2  16841  ncoprmlnprm  16930  prmgaplem5  17259  prmgaplem6  17260  chnfibg  18836  mgmn0plusgf  18853  isnsgrp  18938  isnmnd  18953  dprddomprc  20243  dprddomcld  20244  dprdval0prc  20245  dprdsubg  20267  zrninitoringc  20955  rng1nnzr  21060  rng1nfld  21063  islindf4  22171  nfimdetndef  22931  mdetfval1  22932  dfac14  23964  0nelfb  24177  fbun  24186  opnfbas  24188  trfbas2  24189  isfil2  24202  fsubbas  24213  fbasrn  24230  rnelfmlem  24298  tsmsfbas  24474  ustfilxp  24559  metustfbas  24903  iccpnfcnv  25292  zclmncvs  25496  cphsqrtcl2  25534  minveclem3b  25776  2sq2  27787  vtxvalprc  29650  iedgvalprc  29651  umgrnloop2  29751  nbuhgr  29951  nbumgr  29955  uhgrnbgr0nb  29962  nbgr0vtx  29963  nbgr0edglem  29964  nbgr1vtx  29966  nbgrnself  29967  nbgrnself2  29968  nbgrssovtx  29969  nbgrssvwo2  29970  nbupgrres  29972  nbusgrvtxm1  29987  nb3grprlem2  29989  1hevtxdg0  30113  p1evtxdeqlem  30120  rgrx0ndm  30201  wlkreslem  30275  dfpth2  30341  pthdlem2lem  30380  wwlksnfi  30522  clwwlkneq0  30647  clwwlknnn  30651  clwwlknon1nloop  30717  clwwlknon1sn  30718  eupth2lem3lem6  30861  nfrgr2v  30900  1to2vfriswmgr  30907  4cyclusnfrgr  30920  frgrnbnb  30921  frgrncvvdeqlem1  30927  frgrncvvdeqlem7  30933  frgrncvvdeqlem8  30934  frgrncvvdeqlem9  30935  frgrwopreg  30951  frgrregord013  31023  lpni  31109  evlextv  34241  constrsqrtcl  34478  xrge0iifcnv  34632  noinfepfnregs  35899  noinfepregs  35900  satf0n0  36309  fmlafvel  36316  fmlaomn0  36321  fmlan0  36322  tailfb  37342  dfac21  44259  dvgrat  45486  cvgdvgrat  45487  rusbcALT  45611  fsetsnprcnex  48328  fsetprcnexALT  48335  aiota0ndef  48370  ndfatafv2nrn  48494  afv2ndefb  48497  dfatafv2rnb  48500  fafv2elrnb  48508  afv2ndeffv0  48533  nelbrnel  48549  nelbrnelim  48550  fvmptrab  48565  readdcnnred  48576  resubcnnred  48577  recnmulnred  48578  cndivrenred  48579  sqrtnegnre  48580  0nelsetpreimafv  48675  spr0nelg  48761  spr0el  48767  prminf2  48876  indprm  48917  indprmfz  48918  requad01  48922  0noddALTV  48990  1nevenALTV  48992  2noddALTV  48994  nn0o1gt2ALTV  48995  nn0oALTV  48997  341fppr2  49035  9fppr8  49038  clnbgr0vtx  49137  isubgr3stgrlem3  49269  gpg5nbgrvtx03starlem1  49369  gpg5nbgrvtx03starlem2  49370  gpg5nbgrvtx03starlem3  49371  gpg5nbgrvtx13starlem1  49372  gpg5nbgrvtx13starlem2  49373  gpg5nbgrvtx13starlem3  49374  gpg5nbgrvtx03star  49381  gpg5nbgr3star  49382  lidldomnnring  49536  2zrngnring  49558  cznnring  49562  pgrpgt2nabl  49681  lmod1zrnlvec  49809  lvecpsslmod  49822  suppdm  49825  elbigolo1  49872  ifnmfalse  51137  aacllem  51217