Definition df-nel 3038

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

This definition is referenced by:  neli  3039  nelir  3040  nelcon3d  3041  neleq12d  3042  nfnel  3045  nfneld  3046  nnel  3047  elnelne1  3048  elnelne2  3049  pm2.24nel  3050  pm2.61danel  3051  ru  3727  ruOLD  3728  ssexnelpss  4057  raldifb  4090  elneldisj  4333  elnelun  4334  sbcnel12g  4355  elpwdifsn  4735  0nelrel  5689  feldmfvelcdm  7036  f1ounsn  7224  snnex  7709  pwnex  7710  ssonprc  7738  resf1extb  7882  opabn1stprc  8008  mpoxneldm  8159  mpoxopoveqd  8168  undefnel  8225  fsetdmprc0  8799  fsetcdmex  8807  fsetexb  8808  fiprc  8988  funsnfsupp  9302  elnel  9529  noinfep  9578  dfac9  10056  fz0  13490  0nelfz1  13494  nelfzo  13616  fvinim0ffz  13741  injresinjlem  13742  ssnn0fi  13944  hashnnn0genn0  14302  hashnemnf  14303  hashinfxadd  14344  wrdlndm  14489  wrdsymb0  14508  pfxnd0  14648  repsundef  14730  repswswrd  14743  rennim  15198  cnpart  15199  sqrtneglem  15225  sqreulem  15319  eqsqrtd  15327  fsumsplitsnun  15714  modfsummods  15753  sqrt2irr0  16215  sumeven  16353  sumodd  16354  lcmfval  16587  lcmfn0val  16589  lcmfcl  16594  lcmfnncl  16595  lcmfeq0b  16596  dvdslcmf  16597  lcmftp  16602  lcmfunsnlem2lem1  16604  lcmfunsnlem2lem2  16605  lcmfunsnlem2  16606  ncoprmlnprm  16695  prmgaplem5  17023  prmgaplem6  17024  chnfibg  18599  isnsgrp  18688  isnmnd  18703  dprddomprc  19974  dprddomcld  19975  dprdval0prc  19976  dprdsubg  19998  zrninitoringc  20650  rng1nnzr  20749  rng1nfld  20753  islindf4  21815  nfimdetndef  22551  mdetfval1  22552  dfac14  23580  0nelfb  23793  fbun  23802  opnfbas  23804  trfbas2  23805  isfil2  23818  fsubbas  23829  fbasrn  23846  rnelfmlem  23914  tsmsfbas  24090  ustfilxp  24175  metustfbas  24519  iccpnfcnv  24908  zclmncvs  25112  cphsqrtcl2  25150  minveclem3b  25392  2sq2  27393  vtxvalprc  29111  iedgvalprc  29112  umgrnloop2  29212  nbuhgr  29409  nbumgr  29413  uhgrnbgr0nb  29420  nbgr0vtx  29421  nbgr0edglem  29422  nbgr1vtx  29424  nbgrnself  29425  nbgrnself2  29426  nbgrssovtx  29427  nbgrssvwo2  29428  nbupgrres  29430  nbusgrvtxm1  29445  nb3grprlem2  29447  1hevtxdg0  29571  p1evtxdeqlem  29578  rgrx0ndm  29659  wlkreslem  29733  dfpth2  29794  pthdlem2lem  29832  wwlksnfi  29971  clwwlkneq0  30096  clwwlknnn  30100  clwwlknon1nloop  30166  clwwlknon1sn  30167  eupth2lem3lem6  30300  nfrgr2v  30339  1to2vfriswmgr  30346  4cyclusnfrgr  30359  frgrnbnb  30360  frgrncvvdeqlem1  30366  frgrncvvdeqlem7  30372  frgrncvvdeqlem8  30373  frgrncvvdeqlem9  30374  frgrwopreg  30390  frgrregord013  30462  lpni  30548  evlextv  33683  constrsqrtcl  33920  xrge0iifcnv  34074  noinfepfnregs  35273  noinfepregs  35274  0nn0m1nnn0  35292  satf0n0  35557  fmlafvel  35564  fmlaomn0  35569  fmlan0  35570  tailfb  36556  dfac21  43491  dvgrat  44736  cvgdvgrat  44737  rusbcALT  44862  nthrucw  47311  fsetsnprcnex  47494  fsetprcnexALT  47501  aiota0ndef  47536  ndfatafv2nrn  47660  afv2ndefb  47663  dfatafv2rnb  47666  fafv2elrnb  47674  afv2ndeffv0  47699  nelbrnel  47715  nelbrnelim  47716  fvmptrab  47731  readdcnnred  47742  resubcnnred  47743  recnmulnred  47744  cndivrenred  47745  sqrtnegnre  47746  0nelsetpreimafv  47841  spr0nelg  47927  spr0el  47933  prminf2  48042  indprm  48083  indprmfz  48084  requad01  48088  0noddALTV  48156  1nevenALTV  48158  2noddALTV  48160  nn0o1gt2ALTV  48161  nn0oALTV  48163  341fppr2  48201  9fppr8  48204  clnbgr0vtx  48303  isubgr3stgrlem3  48435  gpg5nbgrvtx03starlem1  48535  gpg5nbgrvtx03starlem2  48536  gpg5nbgrvtx03starlem3  48537  gpg5nbgrvtx13starlem1  48538  gpg5nbgrvtx13starlem2  48539  gpg5nbgrvtx13starlem3  48540  gpg5nbgrvtx03star  48547  gpg5nbgr3star  48548  lidldomnnring  48703  2zrngnring  48725  cznnring  48729  pgrpgt2nabl  48833  lmod1zrnlvec  48961  lvecpsslmod  48974  suppdm  48977  elbigolo1  49024  ifnmfalse  50229  aacllem  50267