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

Definition df-nel 2570
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 2568 . 2  wff  A  e/  B
41, 2wcel 1721 . . 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  2660  neleq2  2661  nfnel  2663  nfneld  2664  nnel  2665  ru  3120  sbcnel12g  3228  raldifb  3447  pwnss  4325  snnex  4672  ssonprc  4731  eldmrexrnb  5836  mpt2xopoveqd  6431  undefnel  6507  fiprc  7147  ruv  7524  ruALT  7525  noinfep  7570  cardprc  7823  alephprc  7936  dfac9  7972  pnfnre  9083  mnfnre  9084  renepnf  9088  renemnf  9089  ltxrlt  9102  xrltnr  10676  pnfnlt  10681  nltmnf  10682  hashnnn0genn0  11582  hashnemnf  11583  hashclb  11596  hasheq0  11599  hashinfxadd  11614  rennim  11999  cnpart  12000  sqrneglem  12027  sqreulem  12118  eqsqrd  12126  eirr  12759  egt2lt3  12760  sqr2irr  12803  nthruc  12805  pcgcd1  13205  pc2dvds  13207  ramtcl2  13334  odhash3  15165  xrsdsreclblem  16699  pnfnei  17238  mnfnei  17239  dfac14  17603  0nelfb  17816  fbun  17825  opnfbas  17827  trfbas2  17828  isfil2  17841  fsubbas  17852  fbasrn  17869  zfbas  17881  rnelfmlem  17937  tsmsfbas  18110  ustfilxp  18195  metustfbasOLD  18548  metustfbas  18549  iccpnfcnv  18922  cphsqrcl2  19102  minveclem3b  19282  i1f0rn  19527  deg1nn0clb  19966  aaliou3  20221  usgrares1  21377  usgrafilem1  21378  nbusgra  21393  nbgra0nb  21394  nbgranself  21399  nbgrassovt  21400  nbgranself2  21401  nb3graprlem2  21414  cusgrares  21434  vdgrf  21622  lpni  21720  xrge0iifcnv  24272  tailfb  26296  dfac21  27032  rusbcALT  27507  afv0nbfvbi  27882  elnelall  27940  frgrancvvdeqlem1  28133  frgrancvvdeqlem2  28134  frgrancvvdeqlemA  28140  frgrancvvdeqlemB  28141  frgrancvvdeqlemC  28142  ifnmfalse  28220  AnelBC  28221
  Copyright terms: Public domain W3C validator