Definition df-nel 3124

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

This definition is referenced by:  neli  3125  nelir  3126  neleq12d  3127  nfnel  3130  nfneld  3131  nnel  3132  elnelne1  3133  elnelne2  3134  nelcon3d  3135  elnelall  3136  pm2.61danel  3137  ru  3771  ssexnelpss  4090  raldifb  4121  elneldisj  4342  elnelun  4343  sbcnel12g  4363  elpwdifsn  4721  0nelrel  5613  snnex  7480  pwnex  7481  ssonprc  7507  opabn1stprc  7756  mpoxneldm  7878  mpoxopoveqd  7887  undefnel  7944  fiprc  8595  funsnfsupp  8857  elnel  9074  noinfep  9123  dfac9  9562  fz0  12923  0nelfz1  12927  nelfzo  13044  fvinim0ffz  13157  injresinjlem  13158  ssnn0fi  13354  hashnnn0genn0  13704  hashnemnf  13705  hashinfxadd  13747  wrdlndm  13879  ffz0iswrdOLD  13892  wrdsymb0  13901  pfxnd0  14050  repsundef  14133  repswswrd  14146  rennim  14598  cnpart  14599  sqrtneglem  14626  sqreulem  14719  eqsqrtd  14727  fsumsplitsnun  15110  modfsummods  15148  sqrt2irr0  15604  sumeven  15738  sumodd  15739  lcmfval  15965  lcmfn0val  15967  lcmfcl  15972  lcmfnncl  15973  lcmfeq0b  15974  dvdslcmf  15975  lcmftp  15980  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  ncoprmlnprm  16068  prmgaplem5  16391  prmgaplem6  16392  isnsgrp  17905  isnmnd  17915  dprddomprc  19122  dprddomcld  19123  dprdval0prc  19124  dprdsubg  19146  rng1nnzr  20047  rng1nfld  20051  islindf4  20982  nfimdetndef  21198  mdetfval1  21199  dfac14  22226  0nelfb  22439  fbun  22448  opnfbas  22450  trfbas2  22451  isfil2  22464  fsubbas  22475  fbasrn  22492  rnelfmlem  22560  tsmsfbas  22736  ustfilxp  22821  metustfbas  23167  iccpnfcnv  23548  zclmncvs  23752  cphsqrtcl2  23790  minveclem3b  24031  2sq2  26009  vtxvalprc  26830  iedgvalprc  26831  umgrnloop2  26931  nbuhgr  27125  nbumgr  27129  uhgrnbgr0nb  27136  nbgr0vtxlem  27137  nbgr1vtx  27140  nbgrnself  27141  nbgrnself2  27142  nbgrssovtx  27143  nbgrssvwo2  27144  nbupgrres  27146  nbusgrvtxm1  27161  nb3grprlem2  27163  1hevtxdg0  27287  p1evtxdeqlem  27294  rgrx0ndm  27375  wlkreslem  27451  pthdlem2lem  27548  wwlksnfi  27684  clwwlkneq0  27807  clwwlknnn  27811  clwwlknfiOLD  27824  clwwlknon1nloop  27878  clwwlknon1sn  27879  eupth2lem3lem6  28012  nfrgr2v  28051  1to2vfriswmgr  28058  4cyclusnfrgr  28071  frgrnbnb  28072  frgrncvvdeqlem1  28078  frgrncvvdeqlem7  28084  frgrncvvdeqlem8  28085  frgrncvvdeqlem9  28086  frgrwopreg  28102  frgrregord013  28174  lpni  28257  xrge0iifcnv  31176  0nn0m1nnn0  32351  satf0n0  32625  fmlafvel  32632  fmlaomn0  32637  fmlan0  32638  tailfb  33725  dfac21  39715  dvgrat  40693  cvgdvgrat  40694  rusbcALT  40820  aiota0ndef  43344  ndfatafv2nrn  43469  afv2ndefb  43472  dfatafv2rnb  43475  fafv2elrnb  43483  afv2ndeffv0  43508  nelbrnel  43524  nelbrnelim  43525  fvmptrab  43540  readdcnnred  43552  resubcnnred  43553  recnmulnred  43554  cndivrenred  43555  sqrtnegnre  43556  0nelsetpreimafv  43599  spr0nelg  43687  spr0el  43693  prminf2  43799  requad01  43835  0noddALTV  43903  1nevenALTV  43905  2noddALTV  43907  nn0o1gt2ALTV  43908  nn0oALTV  43910  341fppr2  43948  9fppr8  43951  lidldomnnring  44250  2zrngnring  44272  cznnring  44276  zrninitoringc  44391  pgrpgt2nabl  44463  lmod1zrnlvec  44598  lvecpsslmod  44611  suppdm  44614  elbigolo1  44666  ifnmfalse  44911  aacllem  44951