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

Definition df-nel 2927
Description: Define negated membership. (Contributed by NM, 7-Aug-1994.)
Assertion
Ref Expression
df-nel (𝐴𝐵 ↔ ¬ 𝐴𝐵)

Detailed syntax breakdown of Definition df-nel
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wnel 2926 . 2 wff 𝐴𝐵
41, 2wcel 2030 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 196 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neli  2928  nelir  2929  neleq12d  2930  nfnel  2933  nfneld  2934  nnel  2935  elnelne1  2936  elnelne2  2937  nelcon3d  2938  elnelall  2939  pm2.61danel  2940  ru  3467  ssexnelpss  3753  raldifb  3783  elneldisj  3996  elnelun  3997  elneldisjOLD  3998  elnelunOLD  3999  sbcnel12g  4018  elpwdifsn  4352  pwnss  4860  0nelrel  5196  snnex  7008  pwnex  7010  ssonprc  7034  opabn1stprc  7272  mpt2xneldm  7383  mpt2xopoveqd  7392  undefnel  7449  fiprc  8080  funsnfsupp  8340  noinfep  8595  dfac9  8996  fz0  12394  0nelfz1  12398  nelfzo  12514  fvinim0ffz  12627  injresinjlem  12628  ssnn0fi  12824  hashnnn0genn0  13171  hashnemnf  13172  hashinfxadd  13212  ffz0iswrd  13364  wrdsymb0  13371  repsundef  13564  repswswrd  13577  rennim  14023  cnpart  14024  sqrtneglem  14051  sqreulem  14143  eqsqrtd  14151  fsumsplitsnun  14528  fsumsplitsnunOLD  14530  modfsummods  14569  sumeven  15157  sumodd  15158  lcmfval  15381  lcmfn0val  15383  lcmfcl  15388  lcmfnncl  15389  lcmfeq0b  15390  dvdslcmf  15391  lcmftp  15396  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  lcmfunsnlem2  15400  ncoprmlnprm  15483  prmgaplem5  15806  prmgaplem6  15807  isnsgrp  17335  isnmnd  17345  dprddomprc  18445  dprddomcld  18446  dprdval0prc  18447  dprdsubg  18469  rng1nnzr  19322  rng1nfld  19326  islindf4  20225  nfimdetndef  20443  mdetfval1  20444  dfac14  21469  0nelfb  21682  fbun  21691  opnfbas  21693  trfbas2  21694  isfil2  21707  fsubbas  21718  fbasrn  21735  rnelfmlem  21803  tsmsfbas  21978  ustfilxp  22063  metustfbas  22409  iccpnfcnv  22790  zclmncvs  22994  cphsqrtcl2  23032  minveclem3b  23245  vtxvalprc  25982  iedgvalprc  25983  umgrnloop2  26086  nbuhgr  26284  nbumgr  26288  uhgrnbgr0nb  26295  nbgr0vtxlem  26296  nbgr1vtx  26299  nbgrnself  26300  nbgrnself2  26301  nbgrssovtx  26302  nbgrssvwo2  26303  nbgrnself2OLD  26304  nbgrssovtxOLD  26305  nbgrssvwo2OLD  26306  nbupgrres  26310  nbusgrvtxm1  26325  nb3grprlem2  26327  1hevtxdg0  26457  p1evtxdeqlem  26464  rgrx0ndm  26545  wlkreslem  26622  pthdlem2lem  26719  clwwlkneq0  26990  clwwlknnn  26995  clwwlknfi  27008  clwwlknon1nloop  27074  clwwlknon1sn  27075  eupth2lem3lem6  27211  nfrgr2v  27252  1to2vfriswmgr  27259  4cyclusnfrgr  27272  frgrnbnb  27273  frgrncvvdeqlem1  27279  frgrncvvdeqlem7  27285  frgrncvvdeqlem8  27286  frgrncvvdeqlem9  27287  frgrwopreg  27303  frgrregord013  27382  lpni  27462  xrge0iifcnv  30107  tailfb  32497  bj-xpima1sn  33068  bj-xpima1snALT  33069  bj-projval  33109  dfac21  37953  dvgrat  38828  cvgdvgrat  38829  rusbcALT  38957  nelbrnel  41617  nelbrnelim  41618  fvmptrab  41631  prminf2  41825  0noddALTV  41925  1nevenALTV  41927  2noddALTV  41929  nn0o1gt2ALTV  41930  nn0oALTV  41932  spr0nelg  42051  spr0el  42057  lidldomnnring  42255  2zrngnring  42277  cznnring  42281  zrninitoringc  42396  pgrpgt2nabl  42472  lmod1zrnlvec  42608  lvecpsslmod  42621  suppdm  42625  elbigolo1  42676  ifnmfalse  42832  aacllem  42875
  Copyright terms: Public domain W3C validator