MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nel Unicode version

Definition df-nel 2609
Description: Define negated membership. (Contributed by NM, 7-Aug-1994.)
Assertion
Ref Expression
df-nel

Detailed syntax breakdown of Definition df-nel
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2wnel 2607 . 2
41, 2wcel 1756 . . 3
54wn 3 . 2
63, 5wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  neli  2707  nelir  2708  neleq1  2709  neleq2  2710  nfnel  2712  nfneld  2713  nnel  2714  ru  3185  raldifb  3496  sbcnel12g  3678  pwnss  4457  eldmrexrnb  5850  ssonprc  6403  mpt2xopoveqd  6738  undefnel  6797  fiprc  7391  funsnfsupp  7644  noinfep  7865  dfac9  8305  fz0  11465  hashnnn0genn0  12114  hashnemnf  12115  hashinfxadd  12148  ffz0iswrd  12255  lsw0  12267  repsundef  12409  repswswrd  12422  rennim  12728  cnpart  12729  sqrneglem  12756  sqreulem  12847  eqsqrd  12855  dprddomprc  16482  dprddomcld  16483  dprdval0prc  16484  dprdsubg  16521  islindf4  18267  nfimdetndef  18400  mdetfval1  18401  dfac14  19191  0nelfb  19404  fbun  19413  opnfbas  19415  trfbas2  19416  isfil2  19429  fsubbas  19440  fbasrn  19457  rnelfmlem  19525  tsmsfbas  19698  ustfilxp  19787  metustfbasOLD  20140  metustfbas  20141  iccpnfcnv  20516  cphsqrcl2  20705  minveclem3b  20915  usgrares1  23323  usgrafilem1  23324  nbusgra  23339  nbgra0nb  23340  nbgranself  23345  nbgrassovt  23346  nbgranself2  23347  nb3graprlem2  23360  cusgrares  23380  vdgrf  23568  lpni  23666  xrge0iifcnv  26363  tailfb  28598  dfac21  29419  rusbcALT  29693  afv0nbfvbi  30057  elnelall  30116  fsumsplitsnun  30242  modfsummods  30244  nbgrassvwo  30276  nbgrassvwo2  30277  nbhashuvtx1  30533  frgrancvvdeqlem1  30623  frgrancvvdeqlem2  30624  frgrancvvdeqlemA  30630  frgrancvvdeqlemB  30631  frgrancvvdeqlemC  30632  ssnn0fi  30746  pgrpgt2nabel  30769  rng1nnzr  31026  rng1nfld  31027  lmod1zrnlvec  31036  lvecpsslmod  31049  ifnmfalse  31098  AnelBC  31099  bj-xpima1sn  32448  bj-xpima1snALT  32449  bj-projval  32489
  Copyright terms: Public domain W3C validator