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 3129
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 3128 . 2 wff 𝐴𝐵
41, 2wcel 2107 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 207 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neli  3130  nelir  3131  neleq12d  3132  nfnel  3135  nfneld  3136  nnel  3137  elnelne1  3138  elnelne2  3139  nelcon3d  3140  elnelall  3141  pm2.61danel  3142  ru  3775  ssexnelpss  4094  raldifb  4125  elneldisj  4346  elnelun  4347  sbcnel12g  4367  elpwdifsn  4720  0nelrel  5612  snnex  7473  pwnex  7474  ssonprc  7500  opabn1stprc  7752  mpoxneldm  7874  mpoxopoveqd  7883  undefnel  7940  fiprc  8589  funsnfsupp  8851  elnel  9068  noinfep  9117  dfac9  9556  fz0  12917  0nelfz1  12921  nelfzo  13038  fvinim0ffz  13151  injresinjlem  13152  ssnn0fi  13348  hashnnn0genn0  13698  hashnemnf  13699  hashinfxadd  13741  wrdlndm  13874  ffz0iswrdOLD  13887  wrdsymb0  13896  pfxnd0  14045  repsundef  14128  repswswrd  14141  rennim  14593  cnpart  14594  sqrtneglem  14621  sqreulem  14714  eqsqrtd  14722  fsumsplitsnun  15105  modfsummods  15143  sqrt2irr0  15599  sumeven  15733  sumodd  15734  lcmfval  15960  lcmfn0val  15962  lcmfcl  15967  lcmfnncl  15968  lcmfeq0b  15969  dvdslcmf  15970  lcmftp  15975  lcmfunsnlem2lem1  15977  lcmfunsnlem2lem2  15978  lcmfunsnlem2  15979  ncoprmlnprm  16063  prmgaplem5  16386  prmgaplem6  16387  isnsgrp  17900  isnmnd  17910  dprddomprc  19058  dprddomcld  19059  dprdval0prc  19060  dprdsubg  19082  rng1nnzr  19982  rng1nfld  19986  islindf4  20917  nfimdetndef  21133  mdetfval1  21134  dfac14  22161  0nelfb  22374  fbun  22383  opnfbas  22385  trfbas2  22386  isfil2  22399  fsubbas  22410  fbasrn  22427  rnelfmlem  22495  tsmsfbas  22670  ustfilxp  22755  metustfbas  23101  iccpnfcnv  23482  zclmncvs  23686  cphsqrtcl2  23724  minveclem3b  23965  2sq2  25942  vtxvalprc  26763  iedgvalprc  26764  umgrnloop2  26864  nbuhgr  27058  nbumgr  27062  uhgrnbgr0nb  27069  nbgr0vtxlem  27070  nbgr1vtx  27073  nbgrnself  27074  nbgrnself2  27075  nbgrssovtx  27076  nbgrssvwo2  27077  nbupgrres  27079  nbusgrvtxm1  27094  nb3grprlem2  27096  1hevtxdg0  27220  p1evtxdeqlem  27227  rgrx0ndm  27308  wlkreslem  27384  pthdlem2lem  27481  wwlksnfi  27617  clwwlkneq0  27740  clwwlknnn  27744  clwwlknfiOLD  27757  clwwlknon1nloop  27811  clwwlknon1sn  27812  eupth2lem3lem6  27945  nfrgr2v  27984  1to2vfriswmgr  27991  4cyclusnfrgr  28004  frgrnbnb  28005  frgrncvvdeqlem1  28011  frgrncvvdeqlem7  28017  frgrncvvdeqlem8  28018  frgrncvvdeqlem9  28019  frgrwopreg  28035  frgrregord013  28107  lpni  28190  xrge0iifcnv  31081  0nn0m1nnn0  32254  satf0n0  32528  fmlafvel  32535  fmlaomn0  32540  fmlan0  32541  tailfb  33628  dfac21  39550  dvgrat  40528  cvgdvgrat  40529  rusbcALT  40655  aiota0ndef  43180  ndfatafv2nrn  43305  afv2ndefb  43308  dfatafv2rnb  43311  fafv2elrnb  43319  afv2ndeffv0  43344  nelbrnel  43360  nelbrnelim  43361  fvmptrab  43376  readdcnnred  43388  resubcnnred  43389  recnmulnred  43390  cndivrenred  43391  sqrtnegnre  43392  spr0nelg  43489  spr0el  43495  prminf2  43601  requad01  43637  0noddALTV  43705  1nevenALTV  43707  2noddALTV  43709  nn0o1gt2ALTV  43710  nn0oALTV  43712  341fppr2  43750  9fppr8  43753  lidldomnnring  44103  2zrngnring  44125  cznnring  44129  zrninitoringc  44244  pgrpgt2nabl  44316  lmod1zrnlvec  44451  lvecpsslmod  44464  suppdm  44467  elbigolo1  44519  ifnmfalse  44764  aacllem  44804
  Copyright terms: Public domain W3C validator