Definition df-nel 3037

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

This definition is referenced by:  neli  3038  nelir  3039  nelcon3d  3040  neleq12d  3041  nfnel  3044  nfneld  3045  nnel  3046  elnelne1  3047  elnelne2  3048  pm2.24nel  3049  pm2.61danel  3050  ru  3726  ruOLD  3727  ssexnelpss  4056  raldifb  4089  elneldisj  4332  elnelun  4333  sbcnel12g  4354  elpwdifsn  4734  0nelrel  5692  feldmfvelcdm  7038  f1ounsn  7227  snnex  7712  pwnex  7713  ssonprc  7741  resf1extb  7885  opabn1stprc  8011  mpoxneldm  8162  mpoxopoveqd  8171  undefnel  8228  fsetdmprc0  8802  fsetcdmex  8810  fsetexb  8811  fiprc  8991  funsnfsupp  9305  elnel  9532  noinfep  9581  dfac9  10059  fz0  13493  0nelfz1  13497  nelfzo  13619  fvinim0ffz  13744  injresinjlem  13745  ssnn0fi  13947  hashnnn0genn0  14305  hashnemnf  14306  hashinfxadd  14347  wrdlndm  14492  wrdsymb0  14511  pfxnd0  14651  repsundef  14733  repswswrd  14746  rennim  15201  cnpart  15202  sqrtneglem  15228  sqreulem  15322  eqsqrtd  15330  fsumsplitsnun  15717  modfsummods  15756  sqrt2irr0  16218  sumeven  16356  sumodd  16357  lcmfval  16590  lcmfn0val  16592  lcmfcl  16597  lcmfnncl  16598  lcmfeq0b  16599  dvdslcmf  16600  lcmftp  16605  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  ncoprmlnprm  16698  prmgaplem5  17026  prmgaplem6  17027  chnfibg  18602  isnsgrp  18691  isnmnd  18706  dprddomprc  19977  dprddomcld  19978  dprdval0prc  19979  dprdsubg  20001  zrninitoringc  20653  rng1nnzr  20752  rng1nfld  20756  islindf4  21818  nfimdetndef  22554  mdetfval1  22555  dfac14  23583  0nelfb  23796  fbun  23805  opnfbas  23807  trfbas2  23808  isfil2  23821  fsubbas  23832  fbasrn  23849  rnelfmlem  23917  tsmsfbas  24093  ustfilxp  24178  metustfbas  24522  iccpnfcnv  24911  zclmncvs  25115  cphsqrtcl2  25153  minveclem3b  25395  2sq2  27396  vtxvalprc  29114  iedgvalprc  29115  umgrnloop2  29215  nbuhgr  29412  nbumgr  29416  uhgrnbgr0nb  29423  nbgr0vtx  29424  nbgr0edglem  29425  nbgr1vtx  29427  nbgrnself  29428  nbgrnself2  29429  nbgrssovtx  29430  nbgrssvwo2  29431  nbupgrres  29433  nbusgrvtxm1  29448  nb3grprlem2  29450  1hevtxdg0  29574  p1evtxdeqlem  29581  rgrx0ndm  29662  wlkreslem  29736  dfpth2  29797  pthdlem2lem  29835  wwlksnfi  29974  clwwlkneq0  30099  clwwlknnn  30103  clwwlknon1nloop  30169  clwwlknon1sn  30170  eupth2lem3lem6  30303  nfrgr2v  30342  1to2vfriswmgr  30349  4cyclusnfrgr  30362  frgrnbnb  30363  frgrncvvdeqlem1  30369  frgrncvvdeqlem7  30375  frgrncvvdeqlem8  30376  frgrncvvdeqlem9  30377  frgrwopreg  30393  frgrregord013  30465  lpni  30551  evlextv  33686  constrsqrtcl  33923  xrge0iifcnv  34077  noinfepfnregs  35276  noinfepregs  35277  0nn0m1nnn0  35295  satf0n0  35560  fmlafvel  35567  fmlaomn0  35572  fmlan0  35573  tailfb  36559  dfac21  43494  dvgrat  44739  cvgdvgrat  44740  rusbcALT  44865  nthrucw  47316  fsetsnprcnex  47503  fsetprcnexALT  47510  aiota0ndef  47545  ndfatafv2nrn  47669  afv2ndefb  47672  dfatafv2rnb  47675  fafv2elrnb  47683  afv2ndeffv0  47708  nelbrnel  47724  nelbrnelim  47725  fvmptrab  47740  readdcnnred  47751  resubcnnred  47752  recnmulnred  47753  cndivrenred  47754  sqrtnegnre  47755  0nelsetpreimafv  47850  spr0nelg  47936  spr0el  47942  prminf2  48051  indprm  48092  indprmfz  48093  requad01  48097  0noddALTV  48165  1nevenALTV  48167  2noddALTV  48169  nn0o1gt2ALTV  48170  nn0oALTV  48172  341fppr2  48210  9fppr8  48213  clnbgr0vtx  48312  isubgr3stgrlem3  48444  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  lidldomnnring  48712  2zrngnring  48734  cznnring  48738  pgrpgt2nabl  48842  lmod1zrnlvec  48970  lvecpsslmod  48983  suppdm  48986  elbigolo1  49033  ifnmfalse  50238  aacllem  50276