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

Definition df-nel 2601
Description: Define negated membership. (Contributed by NM, 7-Aug-1994.)
Assertion
Ref Expression
df-nel  |-  ( A  e/  B  <->  -.  A  e.  B )

Detailed syntax breakdown of Definition df-nel
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2wnel 2599 . 2  wff  A  e/  B
41, 2wcel 1725 . . 3  wff  A  e.  B
54wn 3 . 2  wff  -.  A  e.  B
63, 5wb 177 1  wff  ( A  e/  B  <->  -.  A  e.  B )
Colors of variables: wff set class
This definition is referenced by:  neleq1  2691  neleq2  2692  nfnel  2694  nfneld  2695  nnel  2696  ru  3152  sbcnel12g  3260  raldifb  3479  pwnss  4357  snnex  4705  ssonprc  4764  eldmrexrnb  5869  mpt2xopoveqd  6464  undefnel  6540  fiprc  7180  ruv  7560  ruALT  7561  noinfep  7606  cardprc  7859  alephprc  7972  dfac9  8008  pnfnre  9119  mnfnre  9120  renepnf  9124  renemnf  9125  ltxrlt  9138  xrltnr  10712  pnfnlt  10717  nltmnf  10718  hashnnn0genn0  11619  hashnemnf  11620  hashclb  11633  hasheq0  11636  hashinfxadd  11651  rennim  12036  cnpart  12037  sqrneglem  12064  sqreulem  12155  eqsqrd  12163  eirr  12796  egt2lt3  12797  sqr2irr  12840  nthruc  12842  pcgcd1  13242  pc2dvds  13244  ramtcl2  13371  odhash3  15202  xrsdsreclblem  16736  pnfnei  17276  mnfnei  17277  dfac14  17642  0nelfb  17855  fbun  17864  opnfbas  17866  trfbas2  17867  isfil2  17880  fsubbas  17891  fbasrn  17908  zfbas  17920  rnelfmlem  17976  tsmsfbas  18149  ustfilxp  18234  metustfbasOLD  18587  metustfbas  18588  iccpnfcnv  18961  cphsqrcl2  19141  minveclem3b  19321  i1f0rn  19566  deg1nn0clb  20005  aaliou3  20260  usgrares1  21416  usgrafilem1  21417  nbusgra  21432  nbgra0nb  21433  nbgranself  21438  nbgrassovt  21439  nbgranself2  21440  nb3graprlem2  21453  cusgrares  21473  vdgrf  21661  lpni  21759  xrge0iifcnv  24311  tailfb  26397  dfac21  27132  rusbcALT  27607  afv0nbfvbi  27982  elnelall  28041  lswrd0  28227  frgrancvvdeqlem1  28356  frgrancvvdeqlem2  28357  frgrancvvdeqlemA  28363  frgrancvvdeqlemB  28364  frgrancvvdeqlemC  28365  ifnmfalse  28443  AnelBC  28444
  Copyright terms: Public domain W3C validator