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 2782
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 2780 . 2 wff 𝐴𝐵
41, 2wcel 1976 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 194 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neli  2884  nelir  2885  neleq12d  2886  nfnel  2889  nfneld  2890  nnel  2891  elnelne1  2892  elnelne2  2893  nelcon3d  2894  ru  3400  ssexnelpss  3681  raldifb  3711  elneldisj  3916  elnelun  3917  sbcnel12g  3936  pwnss  4750  ssonprc  6861  mpt2xneldm  7202  mpt2xopoveqd  7211  undefnel  7268  fiprc  7901  funsnfsupp  8159  noinfep  8417  dfac9  8818  fz0  12184  0nelfz1  12188  nelfzo  12301  fvinim0ffz  12406  injresinjlem  12407  ssnn0fi  12603  hashnnn0genn0  12947  hashnemnf  12948  hashinfxadd  12989  ffz0iswrd  13135  wrdsymb0  13142  repsundef  13317  repswswrd  13330  rennim  13775  cnpart  13776  sqrtneglem  13803  sqreulem  13895  eqsqrtd  13903  fsumsplitsnun  14276  modfsummods  14314  sumeven  14896  sumodd  14897  lcmfval  15120  lcmfn0val  15122  lcmfcl  15127  lcmfnncl  15128  lcmfeq0b  15129  dvdslcmf  15130  lcmftp  15135  lcmfunsnlem2lem1  15137  lcmfunsnlem2lem2  15138  lcmfunsnlem2  15139  ncoprmlnprm  15222  prmgaplem5  15545  prmgaplem6  15546  isnsgrp  17059  isnmnd  17069  dprddomprc  18170  dprddomcld  18171  dprdval0prc  18172  dprdsubg  18194  rng1nnzr  19043  rng1nfld  19047  islindf4  19943  nfimdetndef  20161  mdetfval1  20162  dfac14  21178  0nelfb  21392  fbun  21401  opnfbas  21403  trfbas2  21404  isfil2  21417  fsubbas  21428  fbasrn  21445  rnelfmlem  21513  tsmsfbas  21688  ustfilxp  21773  metustfbas  22119  iccpnfcnv  22498  cphsqrtcl2  22738  minveclem3b  22951  usgrares1  25732  usgrafilem1  25733  nbusgra  25750  nbgra0nb  25751  nbgranself  25756  nbgrassovt  25757  nbgranself2  25758  nbgrassvwo  25759  nbgrassvwo2  25760  nb3graprlem2  25774  cusgrares  25794  vdgrf  26218  nbhashuvtx1  26235  frgrancvvdeqlem1  26350  frgrancvvdeqlem2  26351  frgrancvvdeqlemA  26357  frgrancvvdeqlemB  26358  frgrancvvdeqlemC  26359  lpni  26515  xrge0iifcnv  29100  tailfb  31335  bj-xpima1sn  31919  bj-xpima1snALT  31920  bj-projval  31960  bj-xnex  32028  dfac21  36437  dvgrat  37316  cvgdvgrat  37317  rusbcALT  37445  prminf2  39822  0noddALTV  39922  1nevenALTV  39924  2noddALTV  39926  nn0o1gt2ALTV  39927  nn0oALTV  39929  elnelall  40086  elpwdifsn  40096  opabn1stprc  40112  vtxvalprc  40257  iedgvalprc  40258  umgrnloop2  40357  nbuhgr  40546  nbumgr  40550  uhgrnbgr0nb  40557  nbgr0vtxlem  40558  nbgr1vtx  40561  nbgrnself  40564  nbgrnself2  40566  nbgrssovtx  40567  nbgrssvwo2  40568  nbupgrres  40573  nbusgrvtxm1  40588  nb3grprlem2  40590  1hevtxdg0  40701  p1evtxdeqlem  40709  rgrx0ndm  40774  1wlkreslem  40859  pthdlem2lem  40954  clwwlksnfi  41201  eupth2lem3lem6  41382  nfrgr2v  41423  1to2vfriswmgr  41430  4cyclusnfrgr  41443  frgrnbnb  41444  frgrncvvdeqlem1  41450  frgrncvvdeqlem2  41451  frgrncvvdeqlemA  41457  frgrncvvdeqlemB  41458  frgrncvvdeqlemC  41459  frgrwopreg  41467  av-frgraregord013  41530  lidldomnnring  41701  2zrngnring  41723  cznnring  41729  zrninitoringc  41844  pgrpgt2nabl  41922  lmod1zrnlvec  42058  lvecpsslmod  42071  suppdm  42075  elbigolo1  42130  ifnmfalse  42245  aacllem  42298
  Copyright terms: Public domain W3C validator