Definition df-nel 3038

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 3037	. 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  3039  nelir  3040  nelcon3d  3041  neleq12d  3042  nfnel  3045  nfneld  3046  nnel  3047  elnelne1  3048  elnelne2  3049  pm2.24nel  3050  pm2.61danel  3051  ru  3739  ruOLD  3740  ssexnelpss  4069  raldifb  4102  elneldisj  4345  elnelun  4346  sbcnel12g  4367  elpwdifsn  4746  0nelrel  5686  feldmfvelcdm  7033  f1ounsn  7220  snnex  7705  pwnex  7706  ssonprc  7734  resf1extb  7878  opabn1stprc  8004  mpoxneldm  8156  mpoxopoveqd  8165  undefnel  8222  fsetdmprc0  8796  fsetcdmex  8804  fsetexb  8805  fiprc  8985  funsnfsupp  9299  elnel  9524  noinfep  9573  dfac9  10051  fz0  13459  0nelfz1  13463  nelfzo  13584  fvinim0ffz  13709  injresinjlem  13710  ssnn0fi  13912  hashnnn0genn0  14270  hashnemnf  14271  hashinfxadd  14312  wrdlndm  14457  wrdsymb0  14476  pfxnd0  14616  repsundef  14698  repswswrd  14711  rennim  15166  cnpart  15167  sqrtneglem  15193  sqreulem  15287  eqsqrtd  15295  fsumsplitsnun  15682  modfsummods  15720  sqrt2irr0  16180  sumeven  16318  sumodd  16319  lcmfval  16552  lcmfn0val  16554  lcmfcl  16559  lcmfnncl  16560  lcmfeq0b  16561  dvdslcmf  16562  lcmftp  16567  lcmfunsnlem2lem1  16569  lcmfunsnlem2lem2  16570  lcmfunsnlem2  16571  ncoprmlnprm  16659  prmgaplem5  16987  prmgaplem6  16988  chnfibg  18563  isnsgrp  18652  isnmnd  18667  dprddomprc  19935  dprddomcld  19936  dprdval0prc  19937  dprdsubg  19959  zrninitoringc  20613  rng1nnzr  20712  rng1nfld  20716  islindf4  21797  nfimdetndef  22537  mdetfval1  22538  dfac14  23566  0nelfb  23779  fbun  23788  opnfbas  23790  trfbas2  23791  isfil2  23804  fsubbas  23815  fbasrn  23832  rnelfmlem  23900  tsmsfbas  24076  ustfilxp  24161  metustfbas  24505  iccpnfcnv  24902  zclmncvs  25108  cphsqrtcl2  25146  minveclem3b  25388  2sq2  27404  vtxvalprc  29122  iedgvalprc  29123  umgrnloop2  29223  nbuhgr  29420  nbumgr  29424  uhgrnbgr0nb  29431  nbgr0vtx  29432  nbgr0edglem  29433  nbgr1vtx  29435  nbgrnself  29436  nbgrnself2  29437  nbgrssovtx  29438  nbgrssvwo2  29439  nbupgrres  29441  nbusgrvtxm1  29456  nb3grprlem2  29458  1hevtxdg0  29583  p1evtxdeqlem  29590  rgrx0ndm  29671  wlkreslem  29745  dfpth2  29806  pthdlem2lem  29844  wwlksnfi  29983  clwwlkneq0  30108  clwwlknnn  30112  clwwlknon1nloop  30178  clwwlknon1sn  30179  eupth2lem3lem6  30312  nfrgr2v  30351  1to2vfriswmgr  30358  4cyclusnfrgr  30371  frgrnbnb  30372  frgrncvvdeqlem1  30378  frgrncvvdeqlem7  30384  frgrncvvdeqlem8  30385  frgrncvvdeqlem9  30386  frgrwopreg  30402  frgrregord013  30474  lpni  30559  evlextv  33709  constrsqrtcl  33938  xrge0iifcnv  34092  noinfepfnregs  35290  noinfepregs  35291  0nn0m1nnn0  35309  satf0n0  35574  fmlafvel  35581  fmlaomn0  35586  fmlan0  35587  tailfb  36573  dfac21  43375  dvgrat  44620  cvgdvgrat  44621  rusbcALT  44746  nthrucw  47197  fsetsnprcnex  47368  fsetprcnexALT  47375  aiota0ndef  47410  ndfatafv2nrn  47534  afv2ndefb  47537  dfatafv2rnb  47540  fafv2elrnb  47548  afv2ndeffv0  47573  nelbrnel  47589  nelbrnelim  47590  fvmptrab  47605  readdcnnred  47616  resubcnnred  47617  recnmulnred  47618  cndivrenred  47619  sqrtnegnre  47620  0nelsetpreimafv  47703  spr0nelg  47789  spr0el  47795  prminf2  47901  requad01  47934  0noddALTV  48002  1nevenALTV  48004  2noddALTV  48006  nn0o1gt2ALTV  48007  nn0oALTV  48009  341fppr2  48047  9fppr8  48050  clnbgr0vtx  48149  isubgr3stgrlem3  48281  gpg5nbgrvtx03starlem1  48381  gpg5nbgrvtx03starlem2  48382  gpg5nbgrvtx03starlem3  48383  gpg5nbgrvtx13starlem1  48384  gpg5nbgrvtx13starlem2  48385  gpg5nbgrvtx13starlem3  48386  gpg5nbgrvtx03star  48393  gpg5nbgr3star  48394  lidldomnnring  48549  2zrngnring  48571  cznnring  48575  pgrpgt2nabl  48679  lmod1zrnlvec  48807  lvecpsslmod  48820  suppdm  48823  elbigolo1  48870  ifnmfalse  50075  aacllem  50113