Definition df-nel 3046

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

This definition is referenced by:  neli  3047  nelir  3048  nelcon3d  3049  neleq12d  3050  nfnel  3053  nfneld  3054  nnel  3055  elnelne1  3056  elnelne2  3057  pm2.24nel  3058  pm2.61danel  3059  ru  3741  ssexnelpss  4078  raldifb  4109  elneldisj  4353  elnelun  4354  sbcnel12g  4376  elpwdifsn  4754  0nelrel  5698  snnex  7697  pwnex  7698  ssonprc  7727  opabn1stprc  7995  mpoxneldm  8148  mpoxopoveqd  8157  undefnel  8214  fsetdmprc0  8800  fsetcdmex  8808  fsetexb  8809  fiprc  8996  funsnfsupp  9338  elnel  9556  noinfep  9605  dfac9  10081  fz0  13466  0nelfz1  13470  nelfzo  13587  fvinim0ffz  13701  injresinjlem  13702  ssnn0fi  13900  hashnnn0genn0  14253  hashnemnf  14254  hashinfxadd  14295  wrdlndm  14430  wrdsymb0  14449  pfxnd0  14588  repsundef  14671  repswswrd  14684  rennim  15136  cnpart  15137  sqrtneglem  15163  sqreulem  15256  eqsqrtd  15264  fsumsplitsnun  15651  modfsummods  15689  sqrt2irr0  16144  sumeven  16280  sumodd  16281  lcmfval  16508  lcmfn0val  16510  lcmfcl  16515  lcmfnncl  16516  lcmfeq0b  16517  dvdslcmf  16518  lcmftp  16523  lcmfunsnlem2lem1  16525  lcmfunsnlem2lem2  16526  lcmfunsnlem2  16527  ncoprmlnprm  16614  prmgaplem5  16938  prmgaplem6  16939  isnsgrp  18564  isnmnd  18574  dprddomprc  19793  dprddomcld  19794  dprdval0prc  19795  dprdsubg  19817  rng1nnzr  20261  rng1nfld  20265  islindf4  21281  nfimdetndef  21975  mdetfval1  21976  dfac14  23006  0nelfb  23219  fbun  23228  opnfbas  23230  trfbas2  23231  isfil2  23244  fsubbas  23255  fbasrn  23272  rnelfmlem  23340  tsmsfbas  23516  ustfilxp  23601  metustfbas  23950  iccpnfcnv  24344  zclmncvs  24549  cphsqrtcl2  24587  minveclem3b  24829  2sq2  26818  vtxvalprc  28059  iedgvalprc  28060  umgrnloop2  28160  nbuhgr  28354  nbumgr  28358  uhgrnbgr0nb  28365  nbgr0vtxlem  28366  nbgr1vtx  28369  nbgrnself  28370  nbgrnself2  28371  nbgrssovtx  28372  nbgrssvwo2  28373  nbupgrres  28375  nbusgrvtxm1  28390  nb3grprlem2  28392  1hevtxdg0  28516  p1evtxdeqlem  28523  rgrx0ndm  28604  wlkreslem  28680  pthdlem2lem  28778  wwlksnfi  28914  clwwlkneq0  29036  clwwlknnn  29040  clwwlknon1nloop  29106  clwwlknon1sn  29107  eupth2lem3lem6  29240  nfrgr2v  29279  1to2vfriswmgr  29286  4cyclusnfrgr  29299  frgrnbnb  29300  frgrncvvdeqlem1  29306  frgrncvvdeqlem7  29312  frgrncvvdeqlem8  29313  frgrncvvdeqlem9  29314  frgrwopreg  29330  frgrregord013  29402  lpni  29485  xrge0iifcnv  32603  0nn0m1nnn0  33792  satf0n0  34059  fmlafvel  34066  fmlaomn0  34071  fmlan0  34072  tailfb  34925  dfac21  41451  dvgrat  42714  cvgdvgrat  42715  rusbcALT  42841  fsetsnprcnex  45409  fsetprcnexALT  45416  aiota0ndef  45449  ndfatafv2nrn  45573  afv2ndefb  45576  dfatafv2rnb  45579  fafv2elrnb  45587  afv2ndeffv0  45612  nelbrnel  45628  nelbrnelim  45629  fvmptrab  45644  readdcnnred  45655  resubcnnred  45656  recnmulnred  45657  cndivrenred  45658  sqrtnegnre  45659  0nelsetpreimafv  45702  spr0nelg  45788  spr0el  45794  prminf2  45900  requad01  45933  0noddALTV  46001  1nevenALTV  46003  2noddALTV  46005  nn0o1gt2ALTV  46006  nn0oALTV  46008  341fppr2  46046  9fppr8  46049  lidldomnnring  46348  2zrngnring  46370  cznnring  46374  zrninitoringc  46489  pgrpgt2nabl  46562  lmod1zrnlvec  46695  lvecpsslmod  46708  suppdm  46711  elbigolo1  46763  ifnmfalse  47328  aacllem  47368