Definition df-nel 3037

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

This definition is referenced by:  neli  3038  nelir  3039  nelcon3d  3040  neleq12d  3041  nfnel  3044  nfneld  3045  nnel  3046  elnelne1  3047  elnelne2  3048  pm2.24nel  3049  pm2.61danel  3050  ru  3763  ruOLD  3764  ssexnelpss  4091  raldifb  4124  elneldisj  4367  elnelun  4368  sbcnel12g  4389  elpwdifsn  4765  0nelrel  5715  feldmfvelcdm  7075  f1ounsn  7264  snnex  7750  pwnex  7751  ssonprc  7779  resf1extb  7928  opabn1stprc  8055  mpoxneldm  8209  mpoxopoveqd  8218  undefnel  8275  fsetdmprc0  8867  fsetcdmex  8875  fsetexb  8876  fiprc  9057  funsnfsupp  9402  elnel  9623  noinfep  9672  dfac9  10149  fz0  13554  0nelfz1  13558  nelfzo  13679  fvinim0ffz  13800  injresinjlem  13801  ssnn0fi  14001  hashnnn0genn0  14359  hashnemnf  14360  hashinfxadd  14401  wrdlndm  14546  wrdsymb0  14565  pfxnd0  14704  repsundef  14787  repswswrd  14800  rennim  15256  cnpart  15257  sqrtneglem  15283  sqreulem  15376  eqsqrtd  15384  fsumsplitsnun  15769  modfsummods  15807  sqrt2irr0  16267  sumeven  16404  sumodd  16405  lcmfval  16638  lcmfn0val  16640  lcmfcl  16645  lcmfnncl  16646  lcmfeq0b  16647  dvdslcmf  16648  lcmftp  16653  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  lcmfunsnlem2  16657  ncoprmlnprm  16745  prmgaplem5  17073  prmgaplem6  17074  isnsgrp  18699  isnmnd  18714  dprddomprc  19981  dprddomcld  19982  dprdval0prc  19983  dprdsubg  20005  zrninitoringc  20634  rng1nnzr  20733  rng1nfld  20737  islindf4  21796  nfimdetndef  22525  mdetfval1  22526  dfac14  23554  0nelfb  23767  fbun  23776  opnfbas  23778  trfbas2  23779  isfil2  23792  fsubbas  23803  fbasrn  23820  rnelfmlem  23888  tsmsfbas  24064  ustfilxp  24149  metustfbas  24494  iccpnfcnv  24891  zclmncvs  25098  cphsqrtcl2  25136  minveclem3b  25378  2sq2  27394  vtxvalprc  28970  iedgvalprc  28971  umgrnloop2  29071  nbuhgr  29268  nbumgr  29272  uhgrnbgr0nb  29279  nbgr0vtx  29280  nbgr0edglem  29281  nbgr1vtx  29283  nbgrnself  29284  nbgrnself2  29285  nbgrssovtx  29286  nbgrssvwo2  29287  nbupgrres  29289  nbusgrvtxm1  29304  nb3grprlem2  29306  1hevtxdg0  29431  p1evtxdeqlem  29438  rgrx0ndm  29519  wlkreslem  29595  dfpth2  29657  pthdlem2lem  29695  wwlksnfi  29834  clwwlkneq0  29956  clwwlknnn  29960  clwwlknon1nloop  30026  clwwlknon1sn  30027  eupth2lem3lem6  30160  nfrgr2v  30199  1to2vfriswmgr  30206  4cyclusnfrgr  30219  frgrnbnb  30220  frgrncvvdeqlem1  30226  frgrncvvdeqlem7  30232  frgrncvvdeqlem8  30233  frgrncvvdeqlem9  30234  frgrwopreg  30250  frgrregord013  30322  lpni  30407  constrsqrtcl  33759  xrge0iifcnv  33910  0nn0m1nnn0  35081  satf0n0  35346  fmlafvel  35353  fmlaomn0  35358  fmlan0  35359  tailfb  36341  dfac21  43037  dvgrat  44284  cvgdvgrat  44285  rusbcALT  44411  fsetsnprcnex  47032  fsetprcnexALT  47039  aiota0ndef  47074  ndfatafv2nrn  47198  afv2ndefb  47201  dfatafv2rnb  47204  fafv2elrnb  47212  afv2ndeffv0  47237  nelbrnel  47253  nelbrnelim  47254  fvmptrab  47269  readdcnnred  47280  resubcnnred  47281  recnmulnred  47282  cndivrenred  47283  sqrtnegnre  47284  0nelsetpreimafv  47352  spr0nelg  47438  spr0el  47444  prminf2  47550  requad01  47583  0noddALTV  47651  1nevenALTV  47653  2noddALTV  47655  nn0o1gt2ALTV  47656  nn0oALTV  47658  341fppr2  47696  9fppr8  47699  clnbgr0vtx  47797  isubgr3stgrlem3  47928  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  gpg5nbgrvtx03star  48030  gpg5nbgr3star  48031  lidldomnnring  48159  2zrngnring  48181  cznnring  48185  pgrpgt2nabl  48289  lmod1zrnlvec  48418  lvecpsslmod  48431  suppdm  48434  elbigolo1  48485  ifnmfalse  49575  aacllem  49613