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

Definition df-nel 2604
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 2602 . 2  wff  A  e/  B
41, 2wcel 1726 . . 3  wff  A  e.  B
54wn 3 . 2  wff  -.  A  e.  B
63, 5wb 178 1  wff  ( A  e/  B  <->  -.  A  e.  B )
Colors of variables: wff set class
This definition is referenced by:  neli  2699  nelir  2700  neleq1  2701  neleq2  2702  nfnel  2704  nfneld  2705  nnel  2706  ru  3162  sbcnel12g  3270  raldifb  3489  pwnss  4367  ssonprc  4774  eldmrexrnb  5879  mpt2xopoveqd  6474  undefnel  6550  fiprc  7190  ruALT  7571  noinfep  7616  dfac9  8018  hashnnn0genn0  11629  hashnemnf  11630  hashinfxadd  11661  rennim  12046  cnpart  12047  sqrneglem  12074  sqreulem  12165  eqsqrd  12173  dfac14  17652  0nelfb  17865  fbun  17874  opnfbas  17876  trfbas2  17877  isfil2  17890  fsubbas  17901  fbasrn  17918  rnelfmlem  17986  tsmsfbas  18159  ustfilxp  18244  metustfbasOLD  18597  metustfbas  18598  iccpnfcnv  18971  cphsqrcl2  19151  minveclem3b  19331  usgrares1  21426  usgrafilem1  21427  nbusgra  21442  nbgra0nb  21443  nbgranself  21448  nbgrassovt  21449  nbgranself2  21450  nb3graprlem2  21463  cusgrares  21483  vdgrf  21671  lpni  21769  xrge0iifcnv  24321  tailfb  26408  dfac21  27143  rusbcALT  27618  afv0nbfvbi  27993  elnelall  28053  lswrd0  28283  nbgrassvwo  28317  nbgrassvwo2  28318  nbhashuvtx1  28419  frgrancvvdeqlem1  28481  frgrancvvdeqlem2  28482  frgrancvvdeqlemA  28488  frgrancvvdeqlemB  28489  frgrancvvdeqlemC  28490  ifnmfalse  28568  AnelBC  28569
  Copyright terms: Public domain W3C validator