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

Definition df-nel 2451
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 2449 . 2  wff  A  e/  B
41, 2wcel 1685 . . 3  wff  A  e.  B
54wn 5 . 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:  neleq1  2539  neleq2  2540  nfnel  2542  nfneld  2544  ru  2992  sbcnel12g  3100  snnex  4524  ssonprc  4583  pwnss  6293  undefnel  6299  fiprc  6938  ruv  7310  ruALT  7311  noinfep  7356  cardprc  7609  alephprc  7722  dfac9  7758  pnfnre  8870  mnfnre  8871  renepnf  8875  renemnf  8876  ltxrlt  8889  xrltnr  10458  pnfnlt  10463  nltmnf  10464  hashclb  11347  hasheq0  11348  rennim  11719  cnpart  11720  sqrneglem  11747  sqreulem  11838  eqsqrd  11846  eirr  12478  egt2lt3  12479  sqr2irr  12522  nthruc  12524  pcgcd1  12924  pc2dvds  12926  ramtcl2  13053  odhash3  14882  xrsdsreclblem  16412  pnfnei  16945  mnfnei  16946  dfac14  17307  0nelfb  17521  fbun  17530  opnfbas  17532  trfbas2  17533  isfil2  17546  fsubbas  17557  fbasrn  17574  zfbas  17586  rnelfmlem  17642  tsmsfbas  17805  iccpnfcnv  18437  cphsqrcl2  18617  minveclem3b  18787  i1f0rn  19032  deg1nn0clb  19471  aaliou3  19726  lpni  20839  gltpntl  25472  gltpntl2  25473  bsstr  25528  nbssntr  25529  abhp  25573  tailfb  25726  dfac21  26564  rusbcALT  27039  afv0nbfvbi  27394  ifnmfalse  27494  AnelBC  27495
  Copyright terms: Public domain W3C validator