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 1818 . . 3
54wn 3 . 2
63, 5wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  neli  2792  nelir  2793  neleq12d  2794  neleq1OLD  2796  neleq2OLD  2798  nfnel  2800  nfneld  2801  nnel  2802  nnelOLD  2803  elnelne1  2804  elnelne2  2805  nelcon3d  2806  ru  3326  raldifb  3643  sbcnel12g  3826  ssexnelpss  3892  pwnss  4617  ssonprc  6627  mpt2xopoveqd  6968  undefnel  7026  fiprc  7617  funsnfsupp  7873  noinfep  8097  dfac9  8537  fz0  11730  ssnn0fi  12094  hashnnn0genn0  12416  hashnemnf  12417  hashinfxadd  12453  ffz0iswrd  12568  lsw0  12586  repsundef  12743  repswswrd  12756  rennim  13072  cnpart  13073  sqrtneglem  13100  sqreulem  13192  eqsqrtd  13200  fsumsplitsnun  13570  modfsummods  13607  isnsgrp  15915  isnmnd  15924  dprddomprc  17031  dprddomcld  17032  dprdval0prc  17033  dprdsubg  17071  rng1nnzr  17922  rng1nfld  17926  islindf4  18873  nfimdetndef  19091  mdetfval1  19092  dfac14  20119  0nelfb  20332  fbun  20341  opnfbas  20343  trfbas2  20344  isfil2  20357  fsubbas  20368  fbasrn  20385  rnelfmlem  20453  tsmsfbas  20626  ustfilxp  20715  metustfbasOLD  21068  metustfbas  21069  iccpnfcnv  21444  cphsqrtcl2  21633  minveclem3b  21843  usgrares1  24410  usgrafilem1  24411  nbusgra  24428  nbgra0nb  24429  nbgranself  24434  nbgrassovt  24435  nbgranself2  24436  nbgrassvwo  24437  nbgrassvwo2  24438  nb3graprlem2  24452  cusgrares  24472  vdgrf  24898  nbhashuvtx1  24915  frgrancvvdeqlem1  25030  frgrancvvdeqlem2  25031  frgrancvvdeqlemA  25037  frgrancvvdeqlemB  25038  frgrancvvdeqlemC  25039  lpni  25181  xrge0iifcnv  27915  tailfb  30195  dfac21  31012  dvgrat  31193  cvgdvgrat  31194  rusbcALT  31346  elnelall  32293  elpwdifsn  32296  usgfislem1  32444  usgfisALTlem1  32448  lidldomnnring  32736  2zrngnring  32758  cznnring  32764  zrninitoringc  32879  pgrpgt2nabl  32959  lmod1zrnlvec  33095  lvecpsslmod  33108  ifnmfalse  33157  aacllem  33216  bj-xpima1sn  34513  bj-xpima1snALT  34514  bj-projval  34554
  Copyright terms: Public domain W3C validator