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 2106	. . 3 wff 𝐴 ∈ 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 ∈ 𝐵
6	3, 5	wb 205	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  3776  ssexnelpss  4113  raldifb  4144  elneldisj  4388  elnelun  4389  sbcnel12g  4411  elpwdifsn  4792  0nelrel  5737  snnex  7747  pwnex  7748  ssonprc  7777  opabn1stprc  8046  mpoxneldm  8199  mpoxopoveqd  8208  undefnel  8265  fsetdmprc0  8851  fsetcdmex  8859  fsetexb  8860  fiprc  9047  funsnfsupp  9389  elnel  9608  noinfep  9657  dfac9  10133  fz0  13520  0nelfz1  13524  nelfzo  13641  fvinim0ffz  13755  injresinjlem  13756  ssnn0fi  13954  hashnnn0genn0  14307  hashnemnf  14308  hashinfxadd  14349  wrdlndm  14484  wrdsymb0  14503  pfxnd0  14642  repsundef  14725  repswswrd  14738  rennim  15190  cnpart  15191  sqrtneglem  15217  sqreulem  15310  eqsqrtd  15318  fsumsplitsnun  15705  modfsummods  15743  sqrt2irr0  16198  sumeven  16334  sumodd  16335  lcmfval  16562  lcmfn0val  16564  lcmfcl  16569  lcmfnncl  16570  lcmfeq0b  16571  dvdslcmf  16572  lcmftp  16577  lcmfunsnlem2lem1  16579  lcmfunsnlem2lem2  16580  lcmfunsnlem2  16581  ncoprmlnprm  16668  prmgaplem5  16992  prmgaplem6  16993  isnsgrp  18648  isnmnd  18663  dprddomprc  19911  dprddomcld  19912  dprdval0prc  19913  dprdsubg  19935  rng1nnzr  20539  rng1nfld  20543  islindf4  21612  nfimdetndef  22311  mdetfval1  22312  dfac14  23342  0nelfb  23555  fbun  23564  opnfbas  23566  trfbas2  23567  isfil2  23580  fsubbas  23591  fbasrn  23608  rnelfmlem  23676  tsmsfbas  23852  ustfilxp  23937  metustfbas  24286  iccpnfcnv  24684  zclmncvs  24889  cphsqrtcl2  24927  minveclem3b  25169  2sq2  27160  vtxvalprc  28560  iedgvalprc  28561  umgrnloop2  28661  nbuhgr  28855  nbumgr  28859  uhgrnbgr0nb  28866  nbgr0vtxlem  28867  nbgr1vtx  28870  nbgrnself  28871  nbgrnself2  28872  nbgrssovtx  28873  nbgrssvwo2  28874  nbupgrres  28876  nbusgrvtxm1  28891  nb3grprlem2  28893  1hevtxdg0  29017  p1evtxdeqlem  29024  rgrx0ndm  29105  wlkreslem  29181  pthdlem2lem  29279  wwlksnfi  29415  clwwlkneq0  29537  clwwlknnn  29541  clwwlknon1nloop  29607  clwwlknon1sn  29608  eupth2lem3lem6  29741  nfrgr2v  29780  1to2vfriswmgr  29787  4cyclusnfrgr  29800  frgrnbnb  29801  frgrncvvdeqlem1  29807  frgrncvvdeqlem7  29813  frgrncvvdeqlem8  29814  frgrncvvdeqlem9  29815  frgrwopreg  29831  frgrregord013  29903  lpni  29988  xrge0iifcnv  33199  0nn0m1nnn0  34388  satf0n0  34655  fmlafvel  34662  fmlaomn0  34667  fmlan0  34668  tailfb  35565  dfac21  42110  dvgrat  43373  cvgdvgrat  43374  rusbcALT  43500  fsetsnprcnex  46064  fsetprcnexALT  46071  aiota0ndef  46104  ndfatafv2nrn  46228  afv2ndefb  46231  dfatafv2rnb  46234  fafv2elrnb  46242  afv2ndeffv0  46267  nelbrnel  46283  nelbrnelim  46284  fvmptrab  46299  readdcnnred  46310  resubcnnred  46311  recnmulnred  46312  cndivrenred  46313  sqrtnegnre  46314  0nelsetpreimafv  46357  spr0nelg  46443  spr0el  46449  prminf2  46555  requad01  46588  0noddALTV  46656  1nevenALTV  46658  2noddALTV  46660  nn0o1gt2ALTV  46661  nn0oALTV  46663  341fppr2  46701  9fppr8  46704  lidldomnnring  46917  2zrngnring  46939  cznnring  46943  zrninitoringc  47058  pgrpgt2nabl  47131  lmod1zrnlvec  47263  lvecpsslmod  47276  suppdm  47279  elbigolo1  47331  ifnmfalse  47896  aacllem  47936