Definition df-nel 3092

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

This definition is referenced by:  neli  3093  nelir  3094  neleq12d  3095  nfnel  3098  nfneld  3099  nnel  3100  elnelne1  3101  elnelne2  3102  nelcon3d  3103  elnelall  3104  pm2.61danel  3105  ru  3719  ssexnelpss  4041  raldifb  4072  elneldisj  4296  elnelun  4297  sbcnel12g  4319  elpwdifsn  4682  0nelrel  5577  snnex  7460  pwnex  7461  ssonprc  7487  opabn1stprc  7738  mpoxneldm  7861  mpoxopoveqd  7870  undefnel  7927  fiprc  8578  funsnfsupp  8841  elnel  9058  noinfep  9107  dfac9  9547  fz0  12917  0nelfz1  12921  nelfzo  13038  fvinim0ffz  13151  injresinjlem  13152  ssnn0fi  13348  hashnnn0genn0  13699  hashnemnf  13700  hashinfxadd  13742  wrdlndm  13873  wrdsymb0  13892  pfxnd0  14041  repsundef  14124  repswswrd  14137  rennim  14590  cnpart  14591  sqrtneglem  14618  sqreulem  14711  eqsqrtd  14719  fsumsplitsnun  15102  modfsummods  15140  sqrt2irr0  15596  sumeven  15728  sumodd  15729  lcmfval  15955  lcmfn0val  15957  lcmfcl  15962  lcmfnncl  15963  lcmfeq0b  15964  dvdslcmf  15965  lcmftp  15970  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  ncoprmlnprm  16058  prmgaplem5  16381  prmgaplem6  16382  isnsgrp  17897  isnmnd  17907  dprddomprc  19115  dprddomcld  19116  dprdval0prc  19117  dprdsubg  19139  rng1nnzr  20040  rng1nfld  20044  islindf4  20527  nfimdetndef  21194  mdetfval1  21195  dfac14  22223  0nelfb  22436  fbun  22445  opnfbas  22447  trfbas2  22448  isfil2  22461  fsubbas  22472  fbasrn  22489  rnelfmlem  22557  tsmsfbas  22733  ustfilxp  22818  metustfbas  23164  iccpnfcnv  23549  zclmncvs  23753  cphsqrtcl2  23791  minveclem3b  24032  2sq2  26017  vtxvalprc  26838  iedgvalprc  26839  umgrnloop2  26939  nbuhgr  27133  nbumgr  27137  uhgrnbgr0nb  27144  nbgr0vtxlem  27145  nbgr1vtx  27148  nbgrnself  27149  nbgrnself2  27150  nbgrssovtx  27151  nbgrssvwo2  27152  nbupgrres  27154  nbusgrvtxm1  27169  nb3grprlem2  27171  1hevtxdg0  27295  p1evtxdeqlem  27302  rgrx0ndm  27383  wlkreslem  27459  pthdlem2lem  27556  wwlksnfi  27692  clwwlkneq0  27814  clwwlknnn  27818  clwwlknon1nloop  27884  clwwlknon1sn  27885  eupth2lem3lem6  28018  nfrgr2v  28057  1to2vfriswmgr  28064  4cyclusnfrgr  28077  frgrnbnb  28078  frgrncvvdeqlem1  28084  frgrncvvdeqlem7  28090  frgrncvvdeqlem8  28091  frgrncvvdeqlem9  28092  frgrwopreg  28108  frgrregord013  28180  lpni  28263  xrge0iifcnv  31286  0nn0m1nnn0  32461  satf0n0  32738  fmlafvel  32745  fmlaomn0  32750  fmlan0  32751  tailfb  33838  dfac21  40010  dvgrat  41016  cvgdvgrat  41017  rusbcALT  41143  aiota0ndef  43652  ndfatafv2nrn  43777  afv2ndefb  43780  dfatafv2rnb  43783  fafv2elrnb  43791  afv2ndeffv0  43816  nelbrnel  43832  nelbrnelim  43833  fvmptrab  43848  readdcnnred  43860  resubcnnred  43861  recnmulnred  43862  cndivrenred  43863  sqrtnegnre  43864  0nelsetpreimafv  43907  spr0nelg  43993  spr0el  43999  prminf2  44105  requad01  44139  0noddALTV  44207  1nevenALTV  44209  2noddALTV  44211  nn0o1gt2ALTV  44212  nn0oALTV  44214  341fppr2  44252  9fppr8  44255  lidldomnnring  44554  2zrngnring  44576  cznnring  44580  zrninitoringc  44695  pgrpgt2nabl  44768  lmod1zrnlvec  44903  lvecpsslmod  44916  suppdm  44919  elbigolo1  44971  ifnmfalse  45289  aacllem  45329