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 2783
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 2781 . 2 wff 𝐴𝐵
41, 2wcel 1977 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 195 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neli  2885  nelir  2886  neleq12d  2887  nfnel  2890  nfneld  2891  nnel  2892  elnelne1  2893  elnelne2  2894  nelcon3d  2895  ru  3401  ssexnelpss  3682  raldifb  3712  elneldisj  3917  elnelun  3918  sbcnel12g  3937  pwnss  4756  ssonprc  6884  mpt2xneldm  7225  mpt2xopoveqd  7234  undefnel  7291  fiprc  7924  funsnfsupp  8182  noinfep  8440  dfac9  8841  fz0  12227  0nelfz1  12231  nelfzo  12344  fvinim0ffz  12449  injresinjlem  12450  ssnn0fi  12646  hashnnn0genn0  12993  hashnemnf  12994  hashinfxadd  13035  ffz0iswrd  13187  wrdsymb0  13194  repsundef  13369  repswswrd  13382  rennim  13827  cnpart  13828  sqrtneglem  13855  sqreulem  13947  eqsqrtd  13955  fsumsplitsnun  14328  modfsummods  14366  sumeven  14948  sumodd  14949  lcmfval  15172  lcmfn0val  15174  lcmfcl  15179  lcmfnncl  15180  lcmfeq0b  15181  dvdslcmf  15182  lcmftp  15187  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  ncoprmlnprm  15274  prmgaplem5  15597  prmgaplem6  15598  isnsgrp  17111  isnmnd  17121  dprddomprc  18222  dprddomcld  18223  dprdval0prc  18224  dprdsubg  18246  rng1nnzr  19095  rng1nfld  19099  islindf4  19996  nfimdetndef  20214  mdetfval1  20215  dfac14  21231  0nelfb  21445  fbun  21454  opnfbas  21456  trfbas2  21457  isfil2  21470  fsubbas  21481  fbasrn  21498  rnelfmlem  21566  tsmsfbas  21741  ustfilxp  21826  metustfbas  22172  iccpnfcnv  22551  zclmncvs  22756  cphsqrtcl2  22794  minveclem3b  23007  vtxvalprc  25720  iedgvalprc  25721  umgrnloop2  25817  usgrares1  25939  usgrafilem1  25940  nbusgra  25957  nbgra0nb  25958  nbgranself  25963  nbgrassovt  25964  nbgranself2  25965  nbgrassvwo  25966  nbgrassvwo2  25967  nb3graprlem2  25981  cusgrares  26001  vdgrf  26425  nbhashuvtx1  26442  frgrancvvdeqlem1  26557  frgrancvvdeqlem2  26558  frgrancvvdeqlemA  26564  frgrancvvdeqlemB  26565  frgrancvvdeqlemC  26566  lpni  26722  xrge0iifcnv  29307  tailfb  31542  bj-xpima1sn  32136  bj-xpima1snALT  32137  bj-projval  32177  bj-xnex  32245  dfac21  36654  dvgrat  37533  cvgdvgrat  37534  rusbcALT  37662  prminf2  40038  0noddALTV  40138  1nevenALTV  40140  2noddALTV  40142  nn0o1gt2ALTV  40143  nn0oALTV  40145  elnelall  40302  elpwdifsn  40312  opabn1stprc  40318  nbuhgr  40565  nbumgr  40569  uhgrnbgr0nb  40576  nbgr0vtxlem  40577  nbgr1vtx  40580  nbgrnself  40583  nbgrnself2  40585  nbgrssovtx  40586  nbgrssvwo2  40587  nbupgrres  40592  nbusgrvtxm1  40607  nb3grprlem2  40609  1hevtxdg0  40720  p1evtxdeqlem  40728  rgrx0ndm  40793  1wlkreslem  40878  pthdlem2lem  40973  clwwlksnfi  41220  eupth2lem3lem6  41401  nfrgr2v  41442  1to2vfriswmgr  41449  4cyclusnfrgr  41462  frgrnbnb  41463  frgrncvvdeqlem1  41469  frgrncvvdeqlem2  41470  frgrncvvdeqlemA  41476  frgrncvvdeqlemB  41477  frgrncvvdeqlemC  41478  frgrwopreg  41486  av-frgraregord013  41549  lidldomnnring  41720  2zrngnring  41742  cznnring  41748  zrninitoringc  41863  pgrpgt2nabl  41941  lmod1zrnlvec  42077  lvecpsslmod  42090  suppdm  42094  elbigolo1  42149  ifnmfalse  42303  aacllem  42356
  Copyright terms: Public domain W3C validator