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 1728 . . 3
54wn 3 . 2
63, 5wb 178 1
Colors of variables: wff set class
This definition is referenced by:  neli  2704  nelir  2705  neleq1  2706  neleq2  2707  nfnel  2709  nfneld  2710  nnel  2711  ru  3169  raldifb  3476  sbcnel12g  3656  pwnss  4404  ssonprc  4813  eldmrexrnb  5925  mpt2xopoveqd  6522  undefnel  6598  fiprc  7237  ruALT  7618  noinfep  7663  dfac9  8067  hashnnn0genn0  11678  hashnemnf  11679  hashinfxadd  11710  rennim  12095  cnpart  12096  sqrneglem  12123  sqreulem  12214  eqsqrd  12222  dfac14  17701  0nelfb  17914  fbun  17923  opnfbas  17925  trfbas2  17926  isfil2  17939  fsubbas  17950  fbasrn  17967  rnelfmlem  18035  tsmsfbas  18208  ustfilxp  18293  metustfbasOLD  18646  metustfbas  18647  iccpnfcnv  19020  cphsqrcl2  19200  minveclem3b  19380  usgrares1  21475  usgrafilem1  21476  nbusgra  21491  nbgra0nb  21492  nbgranself  21497  nbgrassovt  21498  nbgranself2  21499  nb3graprlem2  21512  cusgrares  21532  vdgrf  21720  lpni  21818  xrge0iifcnv  24368  tailfb  26517  dfac21  27320  rusbcALT  27795  afv0nbfvbi  28170  elnelall  28230  lswrd0  28459  nbgrassvwo  28493  nbgrassvwo2  28494  nbhashuvtx1  28595  frgrancvvdeqlem1  28657  frgrancvvdeqlem2  28658  frgrancvvdeqlemA  28664  frgrancvvdeqlemB  28665  frgrancvvdeqlemC  28666  ifnmfalse  28744  AnelBC  28745
  Copyright terms: Public domain W3C validator