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 2142	. . 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  3742  ssexnelpss  4070  raldifb  4102  elneldisj  4348  elnelun  4349  sbcnel12g  4378  elpwdifsn  4756  0nelrel  5721  feldmfvelcdm  7081  f1ounsn  7270  snnex  7755  pwnex  7756  ssonprc  7784  resf1extb  7929  opabn1stprc  8053  mpoxneldm  8206  mpoxopoveqd  8215  undefnel  8273  fsetdmprc0  8850  fsetcdmex  8858  fsetexb  8859  fiprc  9039  funsnfsupp  9350  elnel  9578  noinfep  9627  dfac9  10127  fz0  13573  0nelfz1  13577  nelfzo  13700  fvinim0ffz  13825  injresinjlem  13826  ssnn0fi  14028  hashnnn0genn0  14386  hashnemnf  14387  hashinfxadd  14428  wrdlndm  14574  wrdsymb0  14593  pfxnd0  14733  repsundef  14815  repswswrd  14828  rennim  15297  cnpart  15298  sqrtneglem  15324  sqreulem  15418  eqsqrtd  15426  fsumsplitsnun  15813  modfsummods  15852  sqrt2irr0  16313  sumeven  16451  sumodd  16452  lcmfval  16685  lcmfn0val  16687  lcmfcl  16692  lcmfnncl  16693  lcmfeq0b  16694  dvdslcmf  16695  lcmftp  16700  lcmfunsnlem2lem1  16702  lcmfunsnlem2lem2  16703  lcmfunsnlem2  16704  ncoprmlnprm  16793  prmgaplem5  17121  prmgaplem6  17122  chnfibg  18698  isnsgrp  18787  isnmnd  18802  dprddomprc  20078  dprddomcld  20079  dprdval0prc  20080  dprdsubg  20102  zrninitoringc  20786  rng1nnzr  20890  rng1nfld  20893  islindf4  21999  nfimdetndef  22757  mdetfval1  22758  dfac14  23786  0nelfb  23999  fbun  24008  opnfbas  24010  trfbas2  24011  isfil2  24024  fsubbas  24035  fbasrn  24052  rnelfmlem  24120  tsmsfbas  24296  ustfilxp  24381  metustfbas  24725  iccpnfcnv  25114  zclmncvs  25318  cphsqrtcl2  25356  minveclem3b  25598  2sq2  27608  vtxvalprc  29406  iedgvalprc  29407  umgrnloop2  29507  nbuhgr  29704  nbumgr  29708  uhgrnbgr0nb  29715  nbgr0vtx  29716  nbgr0edglem  29717  nbgr1vtx  29719  nbgrnself  29720  nbgrnself2  29721  nbgrssovtx  29722  nbgrssvwo2  29723  nbupgrres  29725  nbusgrvtxm1  29740  nb3grprlem2  29742  1hevtxdg0  29866  p1evtxdeqlem  29873  rgrx0ndm  29954  wlkreslem  30028  dfpth2  30089  pthdlem2lem  30127  wwlksnfi  30266  clwwlkneq0  30391  clwwlknnn  30395  clwwlknon1nloop  30461  clwwlknon1sn  30462  eupth2lem3lem6  30595  nfrgr2v  30634  1to2vfriswmgr  30641  4cyclusnfrgr  30654  frgrnbnb  30655  frgrncvvdeqlem1  30661  frgrncvvdeqlem7  30667  frgrncvvdeqlem8  30668  frgrncvvdeqlem9  30669  frgrwopreg  30685  frgrregord013  30757  lpni  30843  evlextv  33941  constrsqrtcl  34178  xrge0iifcnv  34332  noinfepfnregs  35553  noinfepregs  35554  0nn0m1nnn0  35612  satf0n0  35878  fmlafvel  35885  fmlaomn0  35890  fmlan0  35891  tailfb  36916  dfac21  43821  dvgrat  45050  cvgdvgrat  45051  rusbcALT  45176  fsetsnprcnex  47820  fsetprcnexALT  47827  aiota0ndef  47862  ndfatafv2nrn  47986  afv2ndefb  47989  dfatafv2rnb  47992  fafv2elrnb  48000  afv2ndeffv0  48025  nelbrnel  48041  nelbrnelim  48042  fvmptrab  48057  readdcnnred  48068  resubcnnred  48069  recnmulnred  48070  cndivrenred  48071  sqrtnegnre  48072  0nelsetpreimafv  48167  spr0nelg  48253  spr0el  48259  prminf2  48368  indprm  48409  indprmfz  48410  requad01  48414  0noddALTV  48482  1nevenALTV  48484  2noddALTV  48486  nn0o1gt2ALTV  48487  nn0oALTV  48489  341fppr2  48527  9fppr8  48530  clnbgr0vtx  48629  isubgr3stgrlem3  48761  gpg5nbgrvtx03starlem1  48861  gpg5nbgrvtx03starlem2  48862  gpg5nbgrvtx03starlem3  48863  gpg5nbgrvtx13starlem1  48864  gpg5nbgrvtx13starlem2  48865  gpg5nbgrvtx13starlem3  48866  gpg5nbgrvtx03star  48873  gpg5nbgr3star  48874  lidldomnnring  49029  2zrngnring  49051  cznnring  49055  pgrpgt2nabl  49174  lmod1zrnlvec  49302  lvecpsslmod  49315  suppdm  49318  elbigolo1  49365  ifnmfalse  50569  aacllem  50649