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 3124
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 3123 . 2 wff 𝐴𝐵
41, 2wcel 2105 . . 3 wff 𝐴𝐵
54wn 3 . 2 wff ¬ 𝐴𝐵
63, 5wb 207 1 wff (𝐴𝐵 ↔ ¬ 𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neli  3125  nelir  3126  neleq12d  3127  nfnel  3130  nfneld  3131  nnel  3132  elnelne1  3133  elnelne2  3134  nelcon3d  3135  elnelall  3136  pm2.61danel  3137  ru  3770  ssexnelpss  4089  raldifb  4120  elneldisj  4341  elnelun  4342  sbcnel12g  4362  elpwdifsn  4715  0nelrel  5607  snnex  7468  pwnex  7469  ssonprc  7495  opabn1stprc  7747  mpoxneldm  7869  mpoxopoveqd  7878  undefnel  7935  fiprc  8584  funsnfsupp  8846  elnel  9063  noinfep  9112  dfac9  9551  fz0  12912  0nelfz1  12916  nelfzo  13033  fvinim0ffz  13146  injresinjlem  13147  ssnn0fi  13343  hashnnn0genn0  13693  hashnemnf  13694  hashinfxadd  13736  wrdlndm  13869  ffz0iswrdOLD  13882  wrdsymb0  13891  pfxnd0  14040  repsundef  14123  repswswrd  14136  rennim  14588  cnpart  14589  sqrtneglem  14616  sqreulem  14709  eqsqrtd  14717  fsumsplitsnun  15100  modfsummods  15138  sqrt2irr0  15594  sumeven  15728  sumodd  15729  lcmfval  15955  lcmfn0val  15957  lcmfcl  15962  lcmfnncl  15963  lcmfeq0b  15964  dvdslcmf  15965  lcmftp  15970  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  ncoprmlnprm  16058  prmgaplem5  16381  prmgaplem6  16382  isnsgrp  17895  isnmnd  17905  dprddomprc  19053  dprddomcld  19054  dprdval0prc  19055  dprdsubg  19077  rng1nnzr  19977  rng1nfld  19981  islindf4  20912  nfimdetndef  21128  mdetfval1  21129  dfac14  22156  0nelfb  22369  fbun  22378  opnfbas  22380  trfbas2  22381  isfil2  22394  fsubbas  22405  fbasrn  22422  rnelfmlem  22490  tsmsfbas  22665  ustfilxp  22750  metustfbas  23096  iccpnfcnv  23477  zclmncvs  23681  cphsqrtcl2  23719  minveclem3b  23960  2sq2  25937  vtxvalprc  26758  iedgvalprc  26759  umgrnloop2  26859  nbuhgr  27053  nbumgr  27057  uhgrnbgr0nb  27064  nbgr0vtxlem  27065  nbgr1vtx  27068  nbgrnself  27069  nbgrnself2  27070  nbgrssovtx  27071  nbgrssvwo2  27072  nbupgrres  27074  nbusgrvtxm1  27089  nb3grprlem2  27091  1hevtxdg0  27215  p1evtxdeqlem  27222  rgrx0ndm  27303  wlkreslem  27379  pthdlem2lem  27476  wwlksnfi  27612  clwwlkneq0  27735  clwwlknnn  27739  clwwlknfiOLD  27752  clwwlknon1nloop  27806  clwwlknon1sn  27807  eupth2lem3lem6  27940  nfrgr2v  27979  1to2vfriswmgr  27986  4cyclusnfrgr  27999  frgrnbnb  28000  frgrncvvdeqlem1  28006  frgrncvvdeqlem7  28012  frgrncvvdeqlem8  28013  frgrncvvdeqlem9  28014  frgrwopreg  28030  frgrregord013  28102  lpni  28185  xrge0iifcnv  31076  0nn0m1nnn0  32249  satf0n0  32523  fmlafvel  32530  fmlaomn0  32535  fmlan0  32536  tailfb  33623  dfac21  39546  dvgrat  40524  cvgdvgrat  40525  rusbcALT  40651  aiota0ndef  43176  ndfatafv2nrn  43301  afv2ndefb  43304  dfatafv2rnb  43307  fafv2elrnb  43315  afv2ndeffv0  43340  nelbrnel  43356  nelbrnelim  43357  fvmptrab  43372  readdcnnred  43384  resubcnnred  43385  recnmulnred  43386  cndivrenred  43387  sqrtnegnre  43388  spr0nelg  43485  spr0el  43491  prminf2  43597  requad01  43633  0noddALTV  43701  1nevenALTV  43703  2noddALTV  43705  nn0o1gt2ALTV  43706  nn0oALTV  43708  341fppr2  43746  9fppr8  43749  lidldomnnring  44099  2zrngnring  44121  cznnring  44125  zrninitoringc  44240  pgrpgt2nabl  44312  lmod1zrnlvec  44447  lvecpsslmod  44460  suppdm  44463  elbigolo1  44515  ifnmfalse  44760  aacllem  44800
  Copyright terms: Public domain W3C validator