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  3751  ruOLD  3752  ssexnelpss  4079  raldifb  4112  elneldisj  4355  elnelun  4356  sbcnel12g  4377  elpwdifsn  4753  0nelrel  5699  feldmfvelcdm  7058  f1ounsn  7247  snnex  7734  pwnex  7735  ssonprc  7763  resf1extb  7910  opabn1stprc  8037  mpoxneldm  8191  mpoxopoveqd  8200  undefnel  8257  fsetdmprc0  8828  fsetcdmex  8836  fsetexb  8837  fiprc  9016  funsnfsupp  9343  elnel  9564  noinfep  9613  dfac9  10090  fz0  13500  0nelfz1  13504  nelfzo  13625  fvinim0ffz  13747  injresinjlem  13748  ssnn0fi  13950  hashnnn0genn0  14308  hashnemnf  14309  hashinfxadd  14350  wrdlndm  14495  wrdsymb0  14514  pfxnd0  14653  repsundef  14736  repswswrd  14749  rennim  15205  cnpart  15206  sqrtneglem  15232  sqreulem  15326  eqsqrtd  15334  fsumsplitsnun  15721  modfsummods  15759  sqrt2irr0  16219  sumeven  16357  sumodd  16358  lcmfval  16591  lcmfn0val  16593  lcmfcl  16598  lcmfnncl  16599  lcmfeq0b  16600  dvdslcmf  16601  lcmftp  16606  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  ncoprmlnprm  16698  prmgaplem5  17026  prmgaplem6  17027  isnsgrp  18650  isnmnd  18665  dprddomprc  19932  dprddomcld  19933  dprdval0prc  19934  dprdsubg  19956  zrninitoringc  20585  rng1nnzr  20684  rng1nfld  20688  islindf4  21747  nfimdetndef  22476  mdetfval1  22477  dfac14  23505  0nelfb  23718  fbun  23727  opnfbas  23729  trfbas2  23730  isfil2  23743  fsubbas  23754  fbasrn  23771  rnelfmlem  23839  tsmsfbas  24015  ustfilxp  24100  metustfbas  24445  iccpnfcnv  24842  zclmncvs  25048  cphsqrtcl2  25086  minveclem3b  25328  2sq2  27344  vtxvalprc  28972  iedgvalprc  28973  umgrnloop2  29073  nbuhgr  29270  nbumgr  29274  uhgrnbgr0nb  29281  nbgr0vtx  29282  nbgr0edglem  29283  nbgr1vtx  29285  nbgrnself  29286  nbgrnself2  29287  nbgrssovtx  29288  nbgrssvwo2  29289  nbupgrres  29291  nbusgrvtxm1  29306  nb3grprlem2  29308  1hevtxdg0  29433  p1evtxdeqlem  29440  rgrx0ndm  29521  wlkreslem  29597  dfpth2  29659  pthdlem2lem  29697  wwlksnfi  29836  clwwlkneq0  29958  clwwlknnn  29962  clwwlknon1nloop  30028  clwwlknon1sn  30029  eupth2lem3lem6  30162  nfrgr2v  30201  1to2vfriswmgr  30208  4cyclusnfrgr  30221  frgrnbnb  30222  frgrncvvdeqlem1  30228  frgrncvvdeqlem7  30234  frgrncvvdeqlem8  30235  frgrncvvdeqlem9  30236  frgrwopreg  30252  frgrregord013  30324  lpni  30409  constrsqrtcl  33769  xrge0iifcnv  33923  0nn0m1nnn0  35100  satf0n0  35365  fmlafvel  35372  fmlaomn0  35377  fmlan0  35378  tailfb  36365  dfac21  43055  dvgrat  44301  cvgdvgrat  44302  rusbcALT  44428  fsetsnprcnex  47053  fsetprcnexALT  47060  aiota0ndef  47095  ndfatafv2nrn  47219  afv2ndefb  47222  dfatafv2rnb  47225  fafv2elrnb  47233  afv2ndeffv0  47258  nelbrnel  47274  nelbrnelim  47275  fvmptrab  47290  readdcnnred  47301  resubcnnred  47302  recnmulnred  47303  cndivrenred  47304  sqrtnegnre  47305  0nelsetpreimafv  47388  spr0nelg  47474  spr0el  47480  prminf2  47586  requad01  47619  0noddALTV  47687  1nevenALTV  47689  2noddALTV  47691  nn0o1gt2ALTV  47692  nn0oALTV  47694  341fppr2  47732  9fppr8  47735  clnbgr0vtx  47833  isubgr3stgrlem3  47964  gpg5nbgrvtx03starlem1  48056  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx03starlem3  48058  gpg5nbgrvtx13starlem1  48059  gpg5nbgrvtx13starlem2  48060  gpg5nbgrvtx13starlem3  48061  gpg5nbgrvtx03star  48068  gpg5nbgr3star  48069  lidldomnnring  48221  2zrngnring  48243  cznnring  48247  pgrpgt2nabl  48351  lmod1zrnlvec  48480  lvecpsslmod  48493  suppdm  48496  elbigolo1  48543  ifnmfalse  49749  aacllem  49787