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

Definition df-nel 2449
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 2447 . 2  wff  A  e/  B
41, 2wcel 1684 . . 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  2537  neleq2  2538  nfnel  2540  nfneld  2542  ru  2990  sbcnel12g  3098  pwnss  4176  snnex  4524  ssonprc  4583  undefnel  6303  fiprc  6942  ruv  7314  ruALT  7315  noinfep  7360  cardprc  7613  alephprc  7726  dfac9  7762  pnfnre  8874  mnfnre  8875  renepnf  8879  renemnf  8880  ltxrlt  8893  xrltnr  10462  pnfnlt  10467  nltmnf  10468  hashclb  11352  hasheq0  11353  rennim  11724  cnpart  11725  sqrneglem  11752  sqreulem  11843  eqsqrd  11851  eirr  12483  egt2lt3  12484  sqr2irr  12527  nthruc  12529  pcgcd1  12929  pc2dvds  12931  ramtcl2  13058  odhash3  14887  xrsdsreclblem  16417  pnfnei  16950  mnfnei  16951  dfac14  17312  0nelfb  17526  fbun  17535  opnfbas  17537  trfbas2  17538  isfil2  17551  fsubbas  17562  fbasrn  17579  zfbas  17591  rnelfmlem  17647  tsmsfbas  17810  iccpnfcnv  18442  cphsqrcl2  18622  minveclem3b  18792  i1f0rn  19037  deg1nn0clb  19476  aaliou3  19731  lpni  20846  xrge0iifcnv  23315  gltpntl  26072  gltpntl2  26073  bsstr  26128  nbssntr  26129  abhp  26173  tailfb  26326  dfac21  27164  rusbcALT  27639  afv0nbfvbi  28014  mpt2xopynvov0g  28080  mpt2xopoveqd  28087  nbgra0nb  28144  nbgranself  28149  nbgrassovt  28150  nbgranself2  28151  ifnmfalse  28233  AnelBC  28234
  Copyright terms: Public domain W3C validator