Definition df-nel 3064

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

This definition is used by:  neli  3065  nelir  3066  nelcon3d  3067  neleq12d  3068  nfnel  3071  nfneld  3072  nnel  3073  elnelne1  3074  elnelne2  3075  pm2.24nel  3076  pm2.61danel  3077  ru  3741  ssexnelpss  4068  raldifb  4099  elneldisj  4345  elnelun  4346  sbcnel12g  4375  elpwdifsn  4755  0nelrel  5720  feldmfvelcdm  7082  f1ounsn  7276  snnex  7760  pwnex  7761  ssonprc  7789  resf1extb  7934  opabn1stprc  8058  mpoxneldm  8213  mpoxopoveqd  8222  undefnel  8280  fsetdmprc0  8859  fsetcdmex  8867  fsetexb  8868  fiprc  9054  funsnfsupp  9365  elnel  9593  noinfep  9642  dfac9  10142  0nn0m1nnn0  12678  fz0  13595  0nelfz1  13599  nelfzo  13722  fvinim0ffz  13847  injresinjlem  13848  ssnn0fi  14051  hashnnn0genn0  14409  hashnemnf  14410  hashinfxadd  14451  wrdlndm  14597  wrdsymb0  14616  pfxnd0  14760  repsundef  14844  repswswrd  14857  rennim  15328  cnpart  15329  sqrtneglem  15355  sqreulem  15449  eqsqrtd  15457  fsumsplitsnun  15843  modfsummods  15882  sqrt2irr0  16343  sumeven  16481  sumodd  16482  lcmfval  16715  lcmfn0val  16717  lcmfcl  16722  lcmfnncl  16723  lcmfeq0b  16724  dvdslcmf  16725  lcmftp  16730  lcmfunsnlem2lem1  16732  lcmfunsnlem2lem2  16733  lcmfunsnlem2  16734  ncoprmlnprm  16823  prmgaplem5  17151  prmgaplem6  17152  chnfibg  18728  mgmn0plusgf  18745  isnsgrp  18827  isnmnd  18842  dprddomprc  20130  dprddomcld  20131  dprdval0prc  20132  dprdsubg  20154  zrninitoringc  20839  rng1nnzr  20943  rng1nfld  20946  islindf4  22052  nfimdetndef  22812  mdetfval1  22813  dfac14  23845  0nelfb  24058  fbun  24067  opnfbas  24069  trfbas2  24070  isfil2  24083  fsubbas  24094  fbasrn  24111  rnelfmlem  24179  tsmsfbas  24355  ustfilxp  24440  metustfbas  24784  iccpnfcnv  25173  zclmncvs  25377  cphsqrtcl2  25415  minveclem3b  25657  2sq2  27667  vtxvalprc  29488  iedgvalprc  29489  umgrnloop2  29589  nbuhgr  29789  nbumgr  29793  uhgrnbgr0nb  29800  nbgr0vtx  29801  nbgr0edglem  29802  nbgr1vtx  29804  nbgrnself  29805  nbgrnself2  29806  nbgrssovtx  29807  nbgrssvwo2  29808  nbupgrres  29810  nbusgrvtxm1  29825  nb3grprlem2  29827  1hevtxdg0  29951  p1evtxdeqlem  29958  rgrx0ndm  30039  wlkreslem  30113  dfpth2  30179  pthdlem2lem  30218  wwlksnfi  30360  clwwlkneq0  30485  clwwlknnn  30489  clwwlknon1nloop  30555  clwwlknon1sn  30556  eupth2lem3lem6  30699  nfrgr2v  30738  1to2vfriswmgr  30745  4cyclusnfrgr  30758  frgrnbnb  30759  frgrncvvdeqlem1  30765  frgrncvvdeqlem7  30771  frgrncvvdeqlem8  30772  frgrncvvdeqlem9  30773  frgrwopreg  30789  frgrregord013  30861  lpni  30947  evlextv  34039  constrsqrtcl  34276  xrge0iifcnv  34430  noinfepfnregs  35645  noinfepregs  35646  satf0n0  35944  fmlafvel  35951  fmlaomn0  35956  fmlan0  35957  tailfb  36983  dfac21  43894  dvgrat  45123  cvgdvgrat  45124  rusbcALT  45249  fsetsnprcnex  47930  fsetprcnexALT  47937  aiota0ndef  47972  ndfatafv2nrn  48096  afv2ndefb  48099  dfatafv2rnb  48102  fafv2elrnb  48110  afv2ndeffv0  48135  nelbrnel  48151  nelbrnelim  48152  fvmptrab  48167  readdcnnred  48178  resubcnnred  48179  recnmulnred  48180  cndivrenred  48181  sqrtnegnre  48182  0nelsetpreimafv  48277  spr0nelg  48363  spr0el  48369  prminf2  48478  indprm  48519  indprmfz  48520  requad01  48524  0noddALTV  48592  1nevenALTV  48594  2noddALTV  48596  nn0o1gt2ALTV  48597  nn0oALTV  48599  341fppr2  48637  9fppr8  48640  clnbgr0vtx  48739  isubgr3stgrlem3  48871  gpg5nbgrvtx03starlem1  48971  gpg5nbgrvtx03starlem2  48972  gpg5nbgrvtx03starlem3  48973  gpg5nbgrvtx13starlem1  48974  gpg5nbgrvtx13starlem2  48975  gpg5nbgrvtx13starlem3  48976  gpg5nbgrvtx03star  48983  gpg5nbgr3star  48984  lidldomnnring  49138  2zrngnring  49160  cznnring  49164  pgrpgt2nabl  49283  lmod1zrnlvec  49411  lvecpsslmod  49424  suppdm  49427  elbigolo1  49474  ifnmfalse  50679  aacllem  50759