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  4368  ssonprc  4775  eldmrexrnb  5880  mpt2xopoveqd  6475  undefnel  6551  fiprc  7191  ruALT  7572  noinfep  7617  dfac9  8021  hashnnn0genn0  11632  hashnemnf  11633  hashinfxadd  11664  rennim  12049  cnpart  12050  sqrneglem  12077  sqreulem  12168  eqsqrd  12176  dfac14  17655  0nelfb  17868  fbun  17877  opnfbas  17879  trfbas2  17880  isfil2  17893  fsubbas  17904  fbasrn  17921  rnelfmlem  17989  tsmsfbas  18162  ustfilxp  18247  metustfbasOLD  18600  metustfbas  18601  iccpnfcnv  18974  cphsqrcl2  19154  minveclem3b  19334  usgrares1  21429  usgrafilem1  21430  nbusgra  21445  nbgra0nb  21446  nbgranself  21451  nbgrassovt  21452  nbgranself2  21453  nb3graprlem2  21466  cusgrares  21486  vdgrf  21674  lpni  21772  xrge0iifcnv  24324  tailfb  26420  dfac21  27155  rusbcALT  27630  afv0nbfvbi  28005  elnelall  28065  lswrd0  28295  nbgrassvwo  28329  nbgrassvwo2  28330  nbhashuvtx1  28431  frgrancvvdeqlem1  28493  frgrancvvdeqlem2  28494  frgrancvvdeqlemA  28500  frgrancvvdeqlemB  28501  frgrancvvdeqlemC  28502  ifnmfalse  28580  AnelBC  28581
  Copyright terms: Public domain W3C validator