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 3089
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 3088 . 2 wff 𝐴𝐵
41, 2wcel 2157 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 197 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neli  3090  nelir  3091  neleq12d  3092  nfnel  3095  nfneld  3096  nnel  3097  elnelne1  3098  elnelne2  3099  nelcon3d  3100  elnelall  3101  pm2.61danel  3102  ru  3639  ssexnelpss  3925  raldifb  3956  elneldisj  4168  elnelun  4169  elneldisjOLD  4170  elnelunOLD  4171  sbcnel12g  4189  elpwdifsn  4518  pwnss  5029  0nelrel  5369  snnex  7199  pwnex  7201  ssonprc  7225  opabn1stprc  7463  mpt2xneldm  7576  mpt2xopoveqd  7585  undefnel  7642  fiprc  8281  funsnfsupp  8541  elnel  8756  noinfep  8807  dfac9  9246  fz0  12582  0nelfz1  12586  nelfzo  12702  fvinim0ffz  12814  injresinjlem  12815  ssnn0fi  13011  hashnnn0genn0  13354  hashnemnf  13355  hashinfxadd  13395  ffz0iswrd  13546  wrdsymb0  13553  repsundef  13745  repswswrd  13758  rennim  14205  cnpart  14206  sqrtneglem  14233  sqreulem  14325  eqsqrtd  14333  fsumsplitsnun  14710  fsumsplitsnunOLD  14712  modfsummods  14750  sumeven  15333  sumodd  15334  lcmfval  15556  lcmfn0val  15558  lcmfcl  15563  lcmfnncl  15564  lcmfeq0b  15565  dvdslcmf  15566  lcmftp  15571  lcmfunsnlem2lem1  15573  lcmfunsnlem2lem2  15574  lcmfunsnlem2  15575  ncoprmlnprm  15656  prmgaplem5  15979  prmgaplem6  15980  isnsgrp  17496  isnmnd  17506  dprddomprc  18604  dprddomcld  18605  dprdval0prc  18606  dprdsubg  18628  rng1nnzr  19486  rng1nfld  19490  islindf4  20391  nfimdetndef  20610  mdetfval1  20611  dfac14  21639  0nelfb  21852  fbun  21861  opnfbas  21863  trfbas2  21864  isfil2  21877  fsubbas  21888  fbasrn  21905  rnelfmlem  21973  tsmsfbas  22148  ustfilxp  22233  metustfbas  22579  iccpnfcnv  22960  zclmncvs  23164  cphsqrtcl2  23202  minveclem3b  23417  vtxvalprc  26157  iedgvalprc  26158  umgrnloop2  26262  nbuhgr  26461  nbumgr  26465  uhgrnbgr0nb  26472  nbgr0vtxlem  26473  nbgr1vtx  26476  nbgrnself  26477  nbgrnself2  26478  nbgrssovtx  26479  nbgrssvwo2  26480  nbgrnself2OLD  26481  nbgrssovtxOLD  26482  nbgrssvwo2OLD  26483  nbupgrres  26487  nbusgrvtxm1  26503  nb3grprlem2  26505  1hevtxdg0  26635  p1evtxdeqlem  26642  rgrx0ndm  26723  wlkreslem  26800  pthdlem2lem  26897  clwwlkneq0  27182  clwwlknnn  27187  clwwlknfi  27200  clwwlknon1nloop  27273  clwwlknon1sn  27274  eupth2lem3lem6  27412  nfrgr2v  27453  1to2vfriswmgr  27460  4cyclusnfrgr  27473  frgrnbnb  27474  frgrncvvdeqlem1  27480  frgrncvvdeqlem7  27486  frgrncvvdeqlem8  27487  frgrncvvdeqlem9  27488  frgrwopreg  27504  frgrregord013  27589  lpni  27669  xrge0iifcnv  30310  tailfb  32698  bj-xpima1sn  33255  bj-xpima1snALT  33256  bj-projval  33296  dfac21  38138  dvgrat  39012  cvgdvgrat  39013  rusbcALT  39140  aiota0ndef  41680  ndfatafv2nrn  41811  afv2ndefb  41814  dfatafv2rnb  41817  fafv2elrnb  41825  afv2ndeffv0  41850  nelbrnel  41866  nelbrnelim  41867  fvmptrab  41883  prminf2  42076  0noddALTV  42176  1nevenALTV  42178  2noddALTV  42180  nn0o1gt2ALTV  42181  nn0oALTV  42183  spr0nelg  42295  spr0el  42301  lidldomnnring  42499  2zrngnring  42521  cznnring  42525  zrninitoringc  42640  pgrpgt2nabl  42716  lmod1zrnlvec  42852  lvecpsslmod  42865  suppdm  42869  elbigolo1  42920  ifnmfalse  43076  aacllem  43119
  Copyright terms: Public domain W3C validator