Definition df-nel 3035

Description: Define negated membership. (Contributed by NM, 7-Aug-1994.)

Assertion

Ref	Expression
df-nel	⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)

Detailed syntax breakdown of Definition df-nel

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	wnel 3034	. 2 wff 𝐴 ∉ 𝐵
4	1, 2	wcel 2114	. . 3 wff 𝐴 ∈ 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 ∈ 𝐵
6	3, 5	wb 206	1 wff (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)

This definition is referenced by:  neli  3036  nelir  3037  nelcon3d  3038  neleq12d  3039  nfnel  3042  nfneld  3043  nnel  3044  elnelne1  3045  elnelne2  3046  pm2.24nel  3047  pm2.61danel  3048  ru  3723  ruOLD  3724  ssexnelpss  4049  raldifb  4081  elneldisj  4322  elnelun  4323  sbcnel12g  4344  elpwdifsn  4724  0nelrel  5681  feldmfvelcdm  7027  f1ounsn  7216  snnex  7701  pwnex  7702  ssonprc  7730  resf1extb  7874  opabn1stprc  8000  mpoxneldm  8151  mpoxopoveqd  8160  undefnel  8217  fsetdmprc0  8791  fsetcdmex  8799  fsetexb  8800  fiprc  8980  funsnfsupp  9294  elnel  9521  noinfep  9570  dfac9  10048  fz0  13482  0nelfz1  13486  nelfzo  13608  fvinim0ffz  13733  injresinjlem  13734  ssnn0fi  13936  hashnnn0genn0  14294  hashnemnf  14295  hashinfxadd  14336  wrdlndm  14481  wrdsymb0  14500  pfxnd0  14640  repsundef  14722  repswswrd  14735  rennim  15190  cnpart  15191  sqrtneglem  15217  sqreulem  15311  eqsqrtd  15319  fsumsplitsnun  15706  modfsummods  15745  sqrt2irr0  16207  sumeven  16345  sumodd  16346  lcmfval  16579  lcmfn0val  16581  lcmfcl  16586  lcmfnncl  16587  lcmfeq0b  16588  dvdslcmf  16589  lcmftp  16594  lcmfunsnlem2lem1  16596  lcmfunsnlem2lem2  16597  lcmfunsnlem2  16598  ncoprmlnprm  16687  prmgaplem5  17015  prmgaplem6  17016  chnfibg  18591  isnsgrp  18680  isnmnd  18695  dprddomprc  19966  dprddomcld  19967  dprdval0prc  19968  dprdsubg  19990  zrninitoringc  20642  rng1nnzr  20741  rng1nfld  20745  islindf4  21807  nfimdetndef  22542  mdetfval1  22543  dfac14  23571  0nelfb  23784  fbun  23793  opnfbas  23795  trfbas2  23796  isfil2  23809  fsubbas  23820  fbasrn  23837  rnelfmlem  23905  tsmsfbas  24081  ustfilxp  24166  metustfbas  24510  iccpnfcnv  24899  zclmncvs  25103  cphsqrtcl2  25141  minveclem3b  25383  2sq2  27384  vtxvalprc  29102  iedgvalprc  29103  umgrnloop2  29203  nbuhgr  29400  nbumgr  29404  uhgrnbgr0nb  29411  nbgr0vtx  29412  nbgr0edglem  29413  nbgr1vtx  29415  nbgrnself  29416  nbgrnself2  29417  nbgrssovtx  29418  nbgrssvwo2  29419  nbupgrres  29421  nbusgrvtxm1  29436  nb3grprlem2  29438  1hevtxdg0  29562  p1evtxdeqlem  29569  rgrx0ndm  29650  wlkreslem  29724  dfpth2  29785  pthdlem2lem  29823  wwlksnfi  29962  clwwlkneq0  30087  clwwlknnn  30091  clwwlknon1nloop  30157  clwwlknon1sn  30158  eupth2lem3lem6  30291  nfrgr2v  30330  1to2vfriswmgr  30337  4cyclusnfrgr  30350  frgrnbnb  30351  frgrncvvdeqlem1  30357  frgrncvvdeqlem7  30363  frgrncvvdeqlem8  30364  frgrncvvdeqlem9  30365  frgrwopreg  30381  frgrregord013  30453  lpni  30539  evlextv  33674  constrsqrtcl  33911  xrge0iifcnv  34065  noinfepfnregs  35264  noinfepregs  35265  0nn0m1nnn0  35283  satf0n0  35548  fmlafvel  35555  fmlaomn0  35560  fmlan0  35561  tailfb  36547  dfac21  43482  dvgrat  44727  cvgdvgrat  44728  rusbcALT  44853  nthrucw  47304  fsetsnprcnex  47491  fsetprcnexALT  47498  aiota0ndef  47533  ndfatafv2nrn  47657  afv2ndefb  47660  dfatafv2rnb  47663  fafv2elrnb  47671  afv2ndeffv0  47696  nelbrnel  47712  nelbrnelim  47713  fvmptrab  47728  readdcnnred  47739  resubcnnred  47740  recnmulnred  47741  cndivrenred  47742  sqrtnegnre  47743  0nelsetpreimafv  47838  spr0nelg  47924  spr0el  47930  prminf2  48039  indprm  48080  indprmfz  48081  requad01  48085  0noddALTV  48153  1nevenALTV  48155  2noddALTV  48157  nn0o1gt2ALTV  48158  nn0oALTV  48160  341fppr2  48198  9fppr8  48201  clnbgr0vtx  48300  isubgr3stgrlem3  48432  gpg5nbgrvtx03starlem1  48532  gpg5nbgrvtx03starlem2  48533  gpg5nbgrvtx03starlem3  48534  gpg5nbgrvtx13starlem1  48535  gpg5nbgrvtx13starlem2  48536  gpg5nbgrvtx13starlem3  48537  gpg5nbgrvtx03star  48544  gpg5nbgr3star  48545  lidldomnnring  48700  2zrngnring  48722  cznnring  48726  pgrpgt2nabl  48830  lmod1zrnlvec  48958  lvecpsslmod  48971  suppdm  48974  elbigolo1  49021  ifnmfalse  50226  aacllem  50264