Definition df-nel 3033

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

This definition is referenced by:  neli  3034  nelir  3035  nelcon3d  3036  neleq12d  3037  nfnel  3040  nfneld  3041  nnel  3042  elnelne1  3043  elnelne2  3044  pm2.24nel  3045  pm2.61danel  3046  ru  3734  ruOLD  3735  ssexnelpss  4063  raldifb  4096  elneldisj  4339  elnelun  4340  sbcnel12g  4361  elpwdifsn  4738  0nelrel  5675  feldmfvelcdm  7019  f1ounsn  7206  snnex  7691  pwnex  7692  ssonprc  7720  resf1extb  7864  opabn1stprc  7990  mpoxneldm  8142  mpoxopoveqd  8151  undefnel  8208  fsetdmprc0  8779  fsetcdmex  8787  fsetexb  8788  fiprc  8966  funsnfsupp  9276  elnel  9501  noinfep  9550  dfac9  10028  fz0  13439  0nelfz1  13443  nelfzo  13564  fvinim0ffz  13689  injresinjlem  13690  ssnn0fi  13892  hashnnn0genn0  14250  hashnemnf  14251  hashinfxadd  14292  wrdlndm  14437  wrdsymb0  14456  pfxnd0  14596  repsundef  14678  repswswrd  14691  rennim  15146  cnpart  15147  sqrtneglem  15173  sqreulem  15267  eqsqrtd  15275  fsumsplitsnun  15662  modfsummods  15700  sqrt2irr0  16160  sumeven  16298  sumodd  16299  lcmfval  16532  lcmfn0val  16534  lcmfcl  16539  lcmfnncl  16540  lcmfeq0b  16541  dvdslcmf  16542  lcmftp  16547  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  ncoprmlnprm  16639  prmgaplem5  16967  prmgaplem6  16968  chnfibg  18542  isnsgrp  18631  isnmnd  18646  dprddomprc  19914  dprddomcld  19915  dprdval0prc  19916  dprdsubg  19938  zrninitoringc  20591  rng1nnzr  20690  rng1nfld  20694  islindf4  21775  nfimdetndef  22504  mdetfval1  22505  dfac14  23533  0nelfb  23746  fbun  23755  opnfbas  23757  trfbas2  23758  isfil2  23771  fsubbas  23782  fbasrn  23799  rnelfmlem  23867  tsmsfbas  24043  ustfilxp  24128  metustfbas  24472  iccpnfcnv  24869  zclmncvs  25075  cphsqrtcl2  25113  minveclem3b  25355  2sq2  27371  vtxvalprc  29023  iedgvalprc  29024  umgrnloop2  29124  nbuhgr  29321  nbumgr  29325  uhgrnbgr0nb  29332  nbgr0vtx  29333  nbgr0edglem  29334  nbgr1vtx  29336  nbgrnself  29337  nbgrnself2  29338  nbgrssovtx  29339  nbgrssvwo2  29340  nbupgrres  29342  nbusgrvtxm1  29357  nb3grprlem2  29359  1hevtxdg0  29484  p1evtxdeqlem  29491  rgrx0ndm  29572  wlkreslem  29646  dfpth2  29707  pthdlem2lem  29745  wwlksnfi  29884  clwwlkneq0  30009  clwwlknnn  30013  clwwlknon1nloop  30079  clwwlknon1sn  30080  eupth2lem3lem6  30213  nfrgr2v  30252  1to2vfriswmgr  30259  4cyclusnfrgr  30272  frgrnbnb  30273  frgrncvvdeqlem1  30279  frgrncvvdeqlem7  30285  frgrncvvdeqlem8  30286  frgrncvvdeqlem9  30287  frgrwopreg  30303  frgrregord013  30375  lpni  30460  constrsqrtcl  33792  xrge0iifcnv  33946  0nn0m1nnn0  35157  satf0n0  35422  fmlafvel  35429  fmlaomn0  35434  fmlan0  35435  tailfb  36421  dfac21  43169  dvgrat  44415  cvgdvgrat  44416  rusbcALT  44541  nthrucw  46994  fsetsnprcnex  47165  fsetprcnexALT  47172  aiota0ndef  47207  ndfatafv2nrn  47331  afv2ndefb  47334  dfatafv2rnb  47337  fafv2elrnb  47345  afv2ndeffv0  47370  nelbrnel  47386  nelbrnelim  47387  fvmptrab  47402  readdcnnred  47413  resubcnnred  47414  recnmulnred  47415  cndivrenred  47416  sqrtnegnre  47417  0nelsetpreimafv  47500  spr0nelg  47586  spr0el  47592  prminf2  47698  requad01  47731  0noddALTV  47799  1nevenALTV  47801  2noddALTV  47803  nn0o1gt2ALTV  47804  nn0oALTV  47806  341fppr2  47844  9fppr8  47847  clnbgr0vtx  47946  isubgr3stgrlem3  48078  gpg5nbgrvtx03starlem1  48178  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx03starlem3  48180  gpg5nbgrvtx13starlem1  48181  gpg5nbgrvtx13starlem2  48182  gpg5nbgrvtx13starlem3  48183  gpg5nbgrvtx03star  48190  gpg5nbgr3star  48191  lidldomnnring  48346  2zrngnring  48368  cznnring  48372  pgrpgt2nabl  48476  lmod1zrnlvec  48605  lvecpsslmod  48618  suppdm  48621  elbigolo1  48668  ifnmfalse  49874  aacllem  49912