Definition df-nel 3047

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

This definition is referenced by:  neli  3048  nelir  3049  nelcon3d  3050  neleq12d  3051  nfnel  3054  nfneld  3055  nnel  3056  elnelne1  3057  elnelne2  3058  pm2.24nel  3059  pm2.61danel  3060  ru  3786  ruOLD  3787  ssexnelpss  4116  raldifb  4149  elneldisj  4392  elnelun  4393  sbcnel12g  4414  elpwdifsn  4789  0nelrel  5746  feldmfvelcdm  7106  f1ounsn  7292  snnex  7778  pwnex  7779  ssonprc  7807  resf1extb  7956  opabn1stprc  8083  mpoxneldm  8237  mpoxopoveqd  8246  undefnel  8303  fsetdmprc0  8895  fsetcdmex  8903  fsetexb  8904  fiprc  9085  funsnfsupp  9432  elnel  9651  noinfep  9700  dfac9  10177  fz0  13579  0nelfz1  13583  nelfzo  13704  fvinim0ffz  13825  injresinjlem  13826  ssnn0fi  14026  hashnnn0genn0  14382  hashnemnf  14383  hashinfxadd  14424  wrdlndm  14568  wrdsymb0  14587  pfxnd0  14726  repsundef  14809  repswswrd  14822  rennim  15278  cnpart  15279  sqrtneglem  15305  sqreulem  15398  eqsqrtd  15406  fsumsplitsnun  15791  modfsummods  15829  sqrt2irr0  16287  sumeven  16424  sumodd  16425  lcmfval  16658  lcmfn0val  16660  lcmfcl  16665  lcmfnncl  16666  lcmfeq0b  16667  dvdslcmf  16668  lcmftp  16673  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  ncoprmlnprm  16765  prmgaplem5  17093  prmgaplem6  17094  isnsgrp  18736  isnmnd  18751  dprddomprc  20020  dprddomcld  20021  dprdval0prc  20022  dprdsubg  20044  zrninitoringc  20676  rng1nnzr  20776  rng1nfld  20780  islindf4  21858  nfimdetndef  22595  mdetfval1  22596  dfac14  23626  0nelfb  23839  fbun  23848  opnfbas  23850  trfbas2  23851  isfil2  23864  fsubbas  23875  fbasrn  23892  rnelfmlem  23960  tsmsfbas  24136  ustfilxp  24221  metustfbas  24570  iccpnfcnv  24975  zclmncvs  25182  cphsqrtcl2  25220  minveclem3b  25462  2sq2  27477  vtxvalprc  29062  iedgvalprc  29063  umgrnloop2  29163  nbuhgr  29360  nbumgr  29364  uhgrnbgr0nb  29371  nbgr0vtx  29372  nbgr0edglem  29373  nbgr1vtx  29375  nbgrnself  29376  nbgrnself2  29377  nbgrssovtx  29378  nbgrssvwo2  29379  nbupgrres  29381  nbusgrvtxm1  29396  nb3grprlem2  29398  1hevtxdg0  29523  p1evtxdeqlem  29530  rgrx0ndm  29611  wlkreslem  29687  dfpth2  29749  pthdlem2lem  29787  wwlksnfi  29926  clwwlkneq0  30048  clwwlknnn  30052  clwwlknon1nloop  30118  clwwlknon1sn  30119  eupth2lem3lem6  30252  nfrgr2v  30291  1to2vfriswmgr  30298  4cyclusnfrgr  30311  frgrnbnb  30312  frgrncvvdeqlem1  30318  frgrncvvdeqlem7  30324  frgrncvvdeqlem8  30325  frgrncvvdeqlem9  30326  frgrwopreg  30342  frgrregord013  30414  lpni  30499  xrge0iifcnv  33932  0nn0m1nnn0  35118  satf0n0  35383  fmlafvel  35390  fmlaomn0  35395  fmlan0  35396  tailfb  36378  dfac21  43078  dvgrat  44331  cvgdvgrat  44332  rusbcALT  44458  fsetsnprcnex  47067  fsetprcnexALT  47074  aiota0ndef  47109  ndfatafv2nrn  47233  afv2ndefb  47236  dfatafv2rnb  47239  fafv2elrnb  47247  afv2ndeffv0  47272  nelbrnel  47288  nelbrnelim  47289  fvmptrab  47304  readdcnnred  47315  resubcnnred  47316  recnmulnred  47317  cndivrenred  47318  sqrtnegnre  47319  0nelsetpreimafv  47377  spr0nelg  47463  spr0el  47469  prminf2  47575  requad01  47608  0noddALTV  47676  1nevenALTV  47678  2noddALTV  47680  nn0o1gt2ALTV  47681  nn0oALTV  47683  341fppr2  47721  9fppr8  47724  clnbgr0vtx  47822  isubgr3stgrlem3  47935  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  lidldomnnring  48152  2zrngnring  48174  cznnring  48178  pgrpgt2nabl  48282  lmod1zrnlvec  48411  lvecpsslmod  48424  suppdm  48427  elbigolo1  48478  ifnmfalse  49282  aacllem  49320