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 2113	. . 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  3736  ruOLD  3737  ssexnelpss  4066  raldifb  4099  elneldisj  4342  elnelun  4343  sbcnel12g  4364  elpwdifsn  4743  0nelrel  5683  feldmfvelcdm  7029  f1ounsn  7216  snnex  7701  pwnex  7702  ssonprc  7730  resf1extb  7874  opabn1stprc  8000  mpoxneldm  8152  mpoxopoveqd  8161  undefnel  8218  fsetdmprc0  8790  fsetcdmex  8798  fsetexb  8799  fiprc  8979  funsnfsupp  9293  elnel  9518  noinfep  9567  dfac9  10045  fz0  13453  0nelfz1  13457  nelfzo  13578  fvinim0ffz  13703  injresinjlem  13704  ssnn0fi  13906  hashnnn0genn0  14264  hashnemnf  14265  hashinfxadd  14306  wrdlndm  14451  wrdsymb0  14470  pfxnd0  14610  repsundef  14692  repswswrd  14705  rennim  15160  cnpart  15161  sqrtneglem  15187  sqreulem  15281  eqsqrtd  15289  fsumsplitsnun  15676  modfsummods  15714  sqrt2irr0  16174  sumeven  16312  sumodd  16313  lcmfval  16546  lcmfn0val  16548  lcmfcl  16553  lcmfnncl  16554  lcmfeq0b  16555  dvdslcmf  16556  lcmftp  16561  lcmfunsnlem2lem1  16563  lcmfunsnlem2lem2  16564  lcmfunsnlem2  16565  ncoprmlnprm  16653  prmgaplem5  16981  prmgaplem6  16982  chnfibg  18557  isnsgrp  18646  isnmnd  18661  dprddomprc  19929  dprddomcld  19930  dprdval0prc  19931  dprdsubg  19953  zrninitoringc  20607  rng1nnzr  20706  rng1nfld  20710  islindf4  21791  nfimdetndef  22531  mdetfval1  22532  dfac14  23560  0nelfb  23773  fbun  23782  opnfbas  23784  trfbas2  23785  isfil2  23798  fsubbas  23809  fbasrn  23826  rnelfmlem  23894  tsmsfbas  24070  ustfilxp  24155  metustfbas  24499  iccpnfcnv  24896  zclmncvs  25102  cphsqrtcl2  25140  minveclem3b  25382  2sq2  27398  vtxvalprc  29067  iedgvalprc  29068  umgrnloop2  29168  nbuhgr  29365  nbumgr  29369  uhgrnbgr0nb  29376  nbgr0vtx  29377  nbgr0edglem  29378  nbgr1vtx  29380  nbgrnself  29381  nbgrnself2  29382  nbgrssovtx  29383  nbgrssvwo2  29384  nbupgrres  29386  nbusgrvtxm1  29401  nb3grprlem2  29403  1hevtxdg0  29528  p1evtxdeqlem  29535  rgrx0ndm  29616  wlkreslem  29690  dfpth2  29751  pthdlem2lem  29789  wwlksnfi  29928  clwwlkneq0  30053  clwwlknnn  30057  clwwlknon1nloop  30123  clwwlknon1sn  30124  eupth2lem3lem6  30257  nfrgr2v  30296  1to2vfriswmgr  30303  4cyclusnfrgr  30316  frgrnbnb  30317  frgrncvvdeqlem1  30323  frgrncvvdeqlem7  30329  frgrncvvdeqlem8  30330  frgrncvvdeqlem9  30331  frgrwopreg  30347  frgrregord013  30419  lpni  30504  evlextv  33656  constrsqrtcl  33885  xrge0iifcnv  34039  noinfepfnregs  35237  noinfepregs  35238  0nn0m1nnn0  35256  satf0n0  35521  fmlafvel  35528  fmlaomn0  35533  fmlan0  35534  tailfb  36520  dfac21  43250  dvgrat  44495  cvgdvgrat  44496  rusbcALT  44621  nthrucw  47072  fsetsnprcnex  47243  fsetprcnexALT  47250  aiota0ndef  47285  ndfatafv2nrn  47409  afv2ndefb  47412  dfatafv2rnb  47415  fafv2elrnb  47423  afv2ndeffv0  47448  nelbrnel  47464  nelbrnelim  47465  fvmptrab  47480  readdcnnred  47491  resubcnnred  47492  recnmulnred  47493  cndivrenred  47494  sqrtnegnre  47495  0nelsetpreimafv  47578  spr0nelg  47664  spr0el  47670  prminf2  47776  requad01  47809  0noddALTV  47877  1nevenALTV  47879  2noddALTV  47881  nn0o1gt2ALTV  47882  nn0oALTV  47884  341fppr2  47922  9fppr8  47925  clnbgr0vtx  48024  isubgr3stgrlem3  48156  gpg5nbgrvtx03starlem1  48256  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx03starlem3  48258  gpg5nbgrvtx13starlem1  48259  gpg5nbgrvtx13starlem2  48260  gpg5nbgrvtx13starlem3  48261  gpg5nbgrvtx03star  48268  gpg5nbgr3star  48269  lidldomnnring  48424  2zrngnring  48446  cznnring  48450  pgrpgt2nabl  48554  lmod1zrnlvec  48682  lvecpsslmod  48695  suppdm  48698  elbigolo1  48745  ifnmfalse  49950  aacllem  49988