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

Definition df-nel 2482
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 2480 . 2  wff  A  e/  B
41, 2wcel 1701 . . 3  wff  A  e.  B
54wn 3 . 2  wff  -.  A  e.  B
63, 5wb 176 1  wff  ( A  e/  B  <->  -.  A  e.  B )
Colors of variables: wff set class
This definition is referenced by:  neleq1  2570  neleq2  2571  nfnel  2574  nfneld  2576  ru  3024  sbcnel12g  3132  pwnss  4213  snnex  4561  ssonprc  4620  undefnel  6345  fiprc  6985  ruv  7359  ruALT  7360  noinfep  7405  cardprc  7658  alephprc  7771  dfac9  7807  pnfnre  8919  mnfnre  8920  renepnf  8924  renemnf  8925  ltxrlt  8938  xrltnr  10509  pnfnlt  10514  nltmnf  10515  hashclb  11399  hasheq0  11400  rennim  11771  cnpart  11772  sqrneglem  11799  sqreulem  11890  eqsqrd  11898  eirr  12530  egt2lt3  12531  sqr2irr  12574  nthruc  12576  pcgcd1  12976  pc2dvds  12978  ramtcl2  13105  odhash3  14936  xrsdsreclblem  16473  pnfnei  17006  mnfnei  17007  dfac14  17368  0nelfb  17578  fbun  17587  opnfbas  17589  trfbas2  17590  isfil2  17603  fsubbas  17614  fbasrn  17631  zfbas  17643  rnelfmlem  17699  tsmsfbas  17862  iccpnfcnv  18495  cphsqrcl2  18675  minveclem3b  18845  i1f0rn  19090  deg1nn0clb  19529  aaliou3  19784  lpni  20899  xrge0iifcnv  23388  ustfilxp  23429  metustfbas  23499  tailfb  25475  dfac21  26312  rusbcALT  26787  afv0nbfvbi  27164  eldmrexrnb  27247  mpt2xopynvov0g  27254  mpt2xopoveqd  27261  hashnnn0genn0  27286  hashinfxadd  27291  hashnemnf  27292  hashnfinnn0  27293  nbgra0nb  27378  nbgranself  27383  nbgrassovt  27384  nbgranself2  27385  nb3graprlem2  27398  vdgref  27565  frgrancvvdeqlem1  27622  frgrancvvdeqlem2  27623  frgrancvvdeqlemA  27629  frgrancvvdeqlemB  27630  frgrancvvdeqlemC  27631  ifnmfalse  27682  AnelBC  27683
  Copyright terms: Public domain W3C validator