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

Definition df-nel 2596
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 2594 . 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  2686  neleq2  2687  nfnel  2689  nfneld  2690  nnel  2691  ru  3147  sbcnel12g  3255  raldifb  3474  pwnss  4352  snnex  4699  ssonprc  4758  eldmrexrnb  5863  mpt2xopoveqd  6458  undefnel  6534  fiprc  7174  ruv  7552  ruALT  7553  noinfep  7598  cardprc  7851  alephprc  7964  dfac9  8000  pnfnre  9111  mnfnre  9112  renepnf  9116  renemnf  9117  ltxrlt  9130  xrltnr  10704  pnfnlt  10709  nltmnf  10710  hashnnn0genn0  11610  hashnemnf  11611  hashclb  11624  hasheq0  11627  hashinfxadd  11642  rennim  12027  cnpart  12028  sqrneglem  12055  sqreulem  12146  eqsqrd  12154  eirr  12787  egt2lt3  12788  sqr2irr  12831  nthruc  12833  pcgcd1  13233  pc2dvds  13235  ramtcl2  13362  odhash3  15193  xrsdsreclblem  16727  pnfnei  17267  mnfnei  17268  dfac14  17633  0nelfb  17846  fbun  17855  opnfbas  17857  trfbas2  17858  isfil2  17871  fsubbas  17882  fbasrn  17899  zfbas  17911  rnelfmlem  17967  tsmsfbas  18140  ustfilxp  18225  metustfbasOLD  18578  metustfbas  18579  iccpnfcnv  18952  cphsqrcl2  19132  minveclem3b  19312  i1f0rn  19557  deg1nn0clb  19996  aaliou3  20251  usgrares1  21407  usgrafilem1  21408  nbusgra  21423  nbgra0nb  21424  nbgranself  21429  nbgrassovt  21430  nbgranself2  21431  nb3graprlem2  21444  cusgrares  21464  vdgrf  21652  lpni  21750  xrge0iifcnv  24302  tailfb  26338  dfac21  27074  rusbcALT  27549  afv0nbfvbi  27924  elnelall  27982  frgrancvvdeqlem1  28175  frgrancvvdeqlem2  28176  frgrancvvdeqlemA  28182  frgrancvvdeqlemB  28183  frgrancvvdeqlemC  28184  ifnmfalse  28262  AnelBC  28263
  Copyright terms: Public domain W3C validator