Definition df-nel 3062

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

This definition is used by:  neli  3063  nelir  3064  nelcon3d  3065  neleq12d  3066  nfnel  3069  nfneld  3070  nnel  3071  elnelne1  3072  elnelne2  3073  pm2.24nel  3074  pm2.61danel  3075  ru  3737  ssexnelpss  4064  raldifb  4095  elneldisj  4341  elnelun  4342  sbcnel12g  4371  elpwdifsn  4751  0nelrel  5708  feldmfvelcdm  7074  f1ounsn  7268  snnex  7755  pwnex  7756  ssonprc  7784  resf1extb  7929  opabn1stprc  8052  mpoxneldm  8207  mpoxopoveqd  8216  undefnel  8274  fsetdmprc0  8855  fsetcdmex  8863  fsetexb  8864  fiprc  9050  funsnfsupp  9362  elnel  9590  noinfep  9639  dfac9  10186  0nn0m1nnn0  12722  fz0  13640  0nelfz1  13644  nelfzo  13767  fvinim0ffz  13892  injresinjlem  13893  ssnn0fi  14096  hashnnn0genn0  14454  hashnemnf  14455  hashinfxadd  14496  wrdlndm  14642  wrdsymb0  14661  pfxnd0  14805  repsundef  14889  repswswrd  14902  rennim  15373  cnpart  15374  sqrtneglem  15400  sqreulem  15494  eqsqrtd  15502  fsumsplitsnun  15888  modfsummods  15927  sqrt2irr0  16386  sumeven  16524  sumodd  16525  lcmfval  16758  lcmfn0val  16760  lcmfcl  16765  lcmfnncl  16766  lcmfeq0b  16767  dvdslcmf  16768  lcmftp  16773  lcmfunsnlem2lem1  16775  lcmfunsnlem2lem2  16776  lcmfunsnlem2  16777  ncoprmlnprm  16866  prmgaplem5  17194  prmgaplem6  17195  chnfibg  18771  mgmn0plusgf  18788  isnsgrp  18873  isnmnd  18888  dprddomprc  20177  dprddomcld  20178  dprdval0prc  20179  dprdsubg  20201  zrninitoringc  20889  rng1nnzr  20994  rng1nfld  20997  islindf4  22105  nfimdetndef  22865  mdetfval1  22866  dfac14  23898  0nelfb  24111  fbun  24120  opnfbas  24122  trfbas2  24123  isfil2  24136  fsubbas  24147  fbasrn  24164  rnelfmlem  24232  tsmsfbas  24408  ustfilxp  24493  metustfbas  24837  iccpnfcnv  25226  zclmncvs  25430  cphsqrtcl2  25468  minveclem3b  25710  2sq2  27723  vtxvalprc  29556  iedgvalprc  29557  umgrnloop2  29657  nbuhgr  29857  nbumgr  29861  uhgrnbgr0nb  29868  nbgr0vtx  29869  nbgr0edglem  29870  nbgr1vtx  29872  nbgrnself  29873  nbgrnself2  29874  nbgrssovtx  29875  nbgrssvwo2  29876  nbupgrres  29878  nbusgrvtxm1  29893  nb3grprlem2  29895  1hevtxdg0  30019  p1evtxdeqlem  30026  rgrx0ndm  30107  wlkreslem  30181  dfpth2  30247  pthdlem2lem  30286  wwlksnfi  30428  clwwlkneq0  30553  clwwlknnn  30557  clwwlknon1nloop  30623  clwwlknon1sn  30624  eupth2lem3lem6  30767  nfrgr2v  30806  1to2vfriswmgr  30813  4cyclusnfrgr  30826  frgrnbnb  30827  frgrncvvdeqlem1  30833  frgrncvvdeqlem7  30839  frgrncvvdeqlem8  30840  frgrncvvdeqlem9  30841  frgrwopreg  30857  frgrregord013  30929  lpni  31015  evlextv  34107  constrsqrtcl  34344  xrge0iifcnv  34498  noinfepfnregs  35725  noinfepregs  35726  satf0n0  36064  fmlafvel  36071  fmlaomn0  36076  fmlan0  36077  tailfb  37087  dfac21  44011  dvgrat  45240  cvgdvgrat  45241  rusbcALT  45366  fsetsnprcnex  48047  fsetprcnexALT  48054  aiota0ndef  48089  ndfatafv2nrn  48213  afv2ndefb  48216  dfatafv2rnb  48219  fafv2elrnb  48227  afv2ndeffv0  48252  nelbrnel  48268  nelbrnelim  48269  fvmptrab  48284  readdcnnred  48295  resubcnnred  48296  recnmulnred  48297  cndivrenred  48298  sqrtnegnre  48299  0nelsetpreimafv  48394  spr0nelg  48480  spr0el  48486  prminf2  48595  indprm  48636  indprmfz  48637  requad01  48641  0noddALTV  48709  1nevenALTV  48711  2noddALTV  48713  nn0o1gt2ALTV  48714  nn0oALTV  48716  341fppr2  48754  9fppr8  48757  clnbgr0vtx  48856  isubgr3stgrlem3  48988  gpg5nbgrvtx03starlem1  49088  gpg5nbgrvtx03starlem2  49089  gpg5nbgrvtx03starlem3  49090  gpg5nbgrvtx13starlem1  49091  gpg5nbgrvtx13starlem2  49092  gpg5nbgrvtx13starlem3  49093  gpg5nbgrvtx03star  49100  gpg5nbgr3star  49101  lidldomnnring  49255  2zrngnring  49277  cznnring  49281  pgrpgt2nabl  49400  lmod1zrnlvec  49528  lvecpsslmod  49541  suppdm  49544  elbigolo1  49591  ifnmfalse  50781  aacllem  50861