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

Definition df-nel 2655
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 2653 . 2
41, 2wcel 1732 . . 3
54wn 3 . 2
63, 5wb 178 1
Colors of variables: wff set class
This definition is referenced by:  neli  2751  nelir  2752  neleq1  2753  neleq2  2754  nfnel  2756  nfneld  2757  nnel  2758  ru  3223  raldifb  3533  sbcnel12g  3713  pwnss  4480  eldmrexrnb  5866  ssonprc  6413  mpt2xopoveqd  6704  undefnel  6760  fiprc  7353  ruALT  7736  noinfep  7781  dfac9  8187  fz0  11321  hashnnn0genn0  11963  hashnemnf  11964  hashinfxadd  11997  ffz0iswrd  12102  lsw0  12114  repsundef  12256  repswswrd  12269  rennim  12575  cnpart  12576  sqrneglem  12603  sqreulem  12694  eqsqrd  12702  nfimdetndef  17872  mdetfval1  17873  dfac14  18665  0nelfb  18878  fbun  18887  opnfbas  18889  trfbas2  18890  isfil2  18903  fsubbas  18914  fbasrn  18931  rnelfmlem  18999  tsmsfbas  19172  ustfilxp  19257  metustfbasOLD  19610  metustfbas  19611  iccpnfcnv  19984  cphsqrcl2  20164  minveclem3b  20344  usgrares1  22445  usgrafilem1  22446  nbusgra  22461  nbgra0nb  22462  nbgranself  22467  nbgrassovt  22468  nbgranself2  22469  nb3graprlem2  22482  cusgrares  22502  vdgrf  22690  lpni  22788  xrge0iifcnv  25542  tailfb  27778  dfac21  28567  rusbcALT  28867  afv0nbfvbi  29236  elnelall  29295  fsumsplitsnun  29423  modfsummods  29425  nbgrassvwo  29457  nbgrassvwo2  29458  nbhashuvtx1  29714  frgrancvvdeqlem1  29804  frgrancvvdeqlem2  29805  frgrancvvdeqlemA  29811  frgrancvvdeqlemB  29812  frgrancvvdeqlemC  29813  ifnmfalse  29948  AnelBC  29949
  Copyright terms: Public domain W3C validator