Definition df-nel 3039

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

This definition is referenced by:  neli  3040  nelir  3041  neleq12d  3042  nfnel  3045  nfneld  3046  nnel  3047  elnelne1  3048  elnelne2  3049  nelcon3d  3050  elnelall  3051  pm2.61danel  3052  ru  3678  ssexnelpss  4002  raldifb  4033  elneldisj  4274  elnelun  4275  sbcnel12g  4298  elpwdifsn  4674  0nelrel  5578  snnex  7493  pwnex  7494  ssonprc  7520  opabn1stprc  7774  mpoxneldm  7900  mpoxopoveqd  7909  undefnel  7966  fsetdmprc0  8458  fsetcdmex  8466  fsetexb  8467  fiprc  8636  funsnfsupp  8923  elnel  9140  noinfep  9189  dfac9  9629  fz0  13006  0nelfz1  13010  nelfzo  13127  fvinim0ffz  13240  injresinjlem  13241  ssnn0fi  13437  hashnnn0genn0  13788  hashnemnf  13789  hashinfxadd  13831  wrdlndm  13964  wrdsymb0  13983  pfxnd0  14132  repsundef  14215  repswswrd  14228  rennim  14681  cnpart  14682  sqrtneglem  14709  sqreulem  14802  eqsqrtd  14810  fsumsplitsnun  15196  modfsummods  15234  sqrt2irr0  15689  sumeven  15825  sumodd  15826  lcmfval  16055  lcmfn0val  16057  lcmfcl  16062  lcmfnncl  16063  lcmfeq0b  16064  dvdslcmf  16065  lcmftp  16070  lcmfunsnlem2lem1  16072  lcmfunsnlem2lem2  16073  lcmfunsnlem2  16074  ncoprmlnprm  16161  prmgaplem5  16484  prmgaplem6  16485  isnsgrp  18014  isnmnd  18024  dprddomprc  19234  dprddomcld  19235  dprdval0prc  19236  dprdsubg  19258  rng1nnzr  20159  rng1nfld  20163  islindf4  20647  nfimdetndef  21333  mdetfval1  21334  dfac14  22362  0nelfb  22575  fbun  22584  opnfbas  22586  trfbas2  22587  isfil2  22600  fsubbas  22611  fbasrn  22628  rnelfmlem  22696  tsmsfbas  22872  ustfilxp  22957  metustfbas  23303  iccpnfcnv  23689  zclmncvs  23893  cphsqrtcl2  23931  minveclem3b  24173  2sq2  26161  vtxvalprc  26982  iedgvalprc  26983  umgrnloop2  27083  nbuhgr  27277  nbumgr  27281  uhgrnbgr0nb  27288  nbgr0vtxlem  27289  nbgr1vtx  27292  nbgrnself  27293  nbgrnself2  27294  nbgrssovtx  27295  nbgrssvwo2  27296  nbupgrres  27298  nbusgrvtxm1  27313  nb3grprlem2  27315  1hevtxdg0  27439  p1evtxdeqlem  27446  rgrx0ndm  27527  wlkreslem  27603  pthdlem2lem  27700  wwlksnfi  27836  clwwlkneq0  27958  clwwlknnn  27962  clwwlknon1nloop  28028  clwwlknon1sn  28029  eupth2lem3lem6  28162  nfrgr2v  28201  1to2vfriswmgr  28208  4cyclusnfrgr  28221  frgrnbnb  28222  frgrncvvdeqlem1  28228  frgrncvvdeqlem7  28234  frgrncvvdeqlem8  28235  frgrncvvdeqlem9  28236  frgrwopreg  28252  frgrregord013  28324  lpni  28407  xrge0iifcnv  31447  0nn0m1nnn0  32634  satf0n0  32903  fmlafvel  32910  fmlaomn0  32915  fmlan0  32916  tailfb  34196  dfac21  40447  dvgrat  41452  cvgdvgrat  41453  rusbcALT  41579  fsetsnprcnex  44071  fsetprcnexALT  44078  aiota0ndef  44105  ndfatafv2nrn  44230  afv2ndefb  44233  dfatafv2rnb  44236  fafv2elrnb  44244  afv2ndeffv0  44269  nelbrnel  44285  nelbrnelim  44286  fvmptrab  44301  readdcnnred  44313  resubcnnred  44314  recnmulnred  44315  cndivrenred  44316  sqrtnegnre  44317  0nelsetpreimafv  44360  spr0nelg  44446  spr0el  44452  prminf2  44558  requad01  44591  0noddALTV  44659  1nevenALTV  44661  2noddALTV  44663  nn0o1gt2ALTV  44664  nn0oALTV  44666  341fppr2  44704  9fppr8  44707  lidldomnnring  45006  2zrngnring  45028  cznnring  45032  zrninitoringc  45147  pgrpgt2nabl  45220  lmod1zrnlvec  45353  lvecpsslmod  45366  suppdm  45369  elbigolo1  45421  ifnmfalse  45902  aacllem  45942