Definition df-nel 3050

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 3049	. 2 wff 𝐴 ∉ 𝐵
4	1, 2	wcel 2112	. . 3 wff 𝐴 ∈ 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 ∈ 𝐵
6	3, 5	wb 209	1 wff (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)

This definition is referenced by:  neli  3051  nelir  3052  neleq12d  3053  nfnel  3056  nfneld  3057  nnel  3058  elnelne1  3059  elnelne2  3060  nelcon3d  3061  elnelall  3062  pm2.61danel  3063  ru  3711  ssexnelpss  4045  raldifb  4076  elneldisj  4320  elnelun  4321  sbcnel12g  4343  elpwdifsn  4719  0nelrel  5638  snnex  7583  pwnex  7584  ssonprc  7611  opabn1stprc  7868  mpoxneldm  7996  mpoxopoveqd  8005  undefnel  8062  fsetdmprc0  8578  fsetcdmex  8586  fsetexb  8587  fiprc  8766  funsnfsupp  9057  elnel  9274  noinfep  9323  dfac9  9798  fz0  13175  0nelfz1  13179  nelfzo  13296  fvinim0ffz  13409  injresinjlem  13410  ssnn0fi  13608  hashnnn0genn0  13960  hashnemnf  13961  hashinfxadd  14003  wrdlndm  14136  wrdsymb0  14155  pfxnd0  14304  repsundef  14387  repswswrd  14400  rennim  14853  cnpart  14854  sqrtneglem  14881  sqreulem  14974  eqsqrtd  14982  fsumsplitsnun  15370  modfsummods  15408  sqrt2irr0  15863  sumeven  15999  sumodd  16000  lcmfval  16229  lcmfn0val  16231  lcmfcl  16236  lcmfnncl  16237  lcmfeq0b  16238  dvdslcmf  16239  lcmftp  16244  lcmfunsnlem2lem1  16246  lcmfunsnlem2lem2  16247  lcmfunsnlem2  16248  ncoprmlnprm  16335  prmgaplem5  16659  prmgaplem6  16660  isnsgrp  18269  isnmnd  18279  dprddomprc  19493  dprddomcld  19494  dprdval0prc  19495  dprdsubg  19517  rng1nnzr  20433  rng1nfld  20437  islindf4  20930  nfimdetndef  21621  mdetfval1  21622  dfac14  22652  0nelfb  22865  fbun  22874  opnfbas  22876  trfbas2  22877  isfil2  22890  fsubbas  22901  fbasrn  22918  rnelfmlem  22986  tsmsfbas  23162  ustfilxp  23247  metustfbas  23594  iccpnfcnv  23988  zclmncvs  24192  cphsqrtcl2  24230  minveclem3b  24472  2sq2  26461  vtxvalprc  27293  iedgvalprc  27294  umgrnloop2  27394  nbuhgr  27588  nbumgr  27592  uhgrnbgr0nb  27599  nbgr0vtxlem  27600  nbgr1vtx  27603  nbgrnself  27604  nbgrnself2  27605  nbgrssovtx  27606  nbgrssvwo2  27607  nbupgrres  27609  nbusgrvtxm1  27624  nb3grprlem2  27626  1hevtxdg0  27750  p1evtxdeqlem  27757  rgrx0ndm  27838  wlkreslem  27914  pthdlem2lem  28011  wwlksnfi  28147  clwwlkneq0  28269  clwwlknnn  28273  clwwlknon1nloop  28339  clwwlknon1sn  28340  eupth2lem3lem6  28473  nfrgr2v  28512  1to2vfriswmgr  28519  4cyclusnfrgr  28532  frgrnbnb  28533  frgrncvvdeqlem1  28539  frgrncvvdeqlem7  28545  frgrncvvdeqlem8  28546  frgrncvvdeqlem9  28547  frgrwopreg  28563  frgrregord013  28635  lpni  28718  xrge0iifcnv  31760  0nn0m1nnn0  32946  satf0n0  33215  fmlafvel  33222  fmlaomn0  33227  fmlan0  33228  tailfb  34468  dfac21  40779  dvgrat  41792  cvgdvgrat  41793  rusbcALT  41919  fsetsnprcnex  44409  fsetprcnexALT  44416  aiota0ndef  44449  ndfatafv2nrn  44573  afv2ndefb  44576  dfatafv2rnb  44579  fafv2elrnb  44587  afv2ndeffv0  44612  nelbrnel  44628  nelbrnelim  44629  fvmptrab  44644  readdcnnred  44656  resubcnnred  44657  recnmulnred  44658  cndivrenred  44659  sqrtnegnre  44660  0nelsetpreimafv  44703  spr0nelg  44789  spr0el  44795  prminf2  44901  requad01  44934  0noddALTV  45002  1nevenALTV  45004  2noddALTV  45006  nn0o1gt2ALTV  45007  nn0oALTV  45009  341fppr2  45047  9fppr8  45050  lidldomnnring  45349  2zrngnring  45371  cznnring  45375  zrninitoringc  45490  pgrpgt2nabl  45563  lmod1zrnlvec  45696  lvecpsslmod  45709  suppdm  45712  elbigolo1  45764  ifnmfalse  46324  aacllem  46364