Definition df-nel 3053

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

This definition is referenced by:  neli  3054  nelir  3055  nelcon3d  3056  neleq12d  3057  nfnel  3060  nfneld  3061  nnel  3062  elnelne1  3063  elnelne2  3064  pm2.24nel  3065  pm2.61danel  3066  ru  3802  ruOLD  3803  ssexnelpss  4139  raldifb  4172  elneldisj  4415  elnelun  4416  sbcnel12g  4437  elpwdifsn  4814  0nelrel  5761  feldmfvelcdm  7120  snnex  7793  pwnex  7794  ssonprc  7823  opabn1stprc  8099  mpoxneldm  8253  mpoxopoveqd  8262  undefnel  8319  fsetdmprc0  8913  fsetcdmex  8921  fsetexb  8922  fiprc  9111  funsnfsupp  9461  elnel  9680  noinfep  9729  dfac9  10206  fz0  13599  0nelfz1  13603  nelfzo  13721  fvinim0ffz  13836  injresinjlem  13837  ssnn0fi  14036  hashnnn0genn0  14392  hashnemnf  14393  hashinfxadd  14434  wrdlndm  14578  wrdsymb0  14597  pfxnd0  14736  repsundef  14819  repswswrd  14832  rennim  15288  cnpart  15289  sqrtneglem  15315  sqreulem  15408  eqsqrtd  15416  fsumsplitsnun  15803  modfsummods  15841  sqrt2irr0  16299  sumeven  16435  sumodd  16436  lcmfval  16668  lcmfn0val  16670  lcmfcl  16675  lcmfnncl  16676  lcmfeq0b  16677  dvdslcmf  16678  lcmftp  16683  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  lcmfunsnlem2  16687  ncoprmlnprm  16775  prmgaplem5  17102  prmgaplem6  17103  isnsgrp  18761  isnmnd  18776  dprddomprc  20044  dprddomcld  20045  dprdval0prc  20046  dprdsubg  20068  zrninitoringc  20698  rng1nnzr  20798  rng1nfld  20802  islindf4  21881  nfimdetndef  22616  mdetfval1  22617  dfac14  23647  0nelfb  23860  fbun  23869  opnfbas  23871  trfbas2  23872  isfil2  23885  fsubbas  23896  fbasrn  23913  rnelfmlem  23981  tsmsfbas  24157  ustfilxp  24242  metustfbas  24591  iccpnfcnv  24994  zclmncvs  25201  cphsqrtcl2  25239  minveclem3b  25481  2sq2  27495  vtxvalprc  29080  iedgvalprc  29081  umgrnloop2  29181  nbuhgr  29378  nbumgr  29382  uhgrnbgr0nb  29389  nbgr0vtx  29390  nbgr0edglem  29391  nbgr1vtx  29393  nbgrnself  29394  nbgrnself2  29395  nbgrssovtx  29396  nbgrssvwo2  29397  nbupgrres  29399  nbusgrvtxm1  29414  nb3grprlem2  29416  1hevtxdg0  29541  p1evtxdeqlem  29548  rgrx0ndm  29629  wlkreslem  29705  pthdlem2lem  29803  wwlksnfi  29939  clwwlkneq0  30061  clwwlknnn  30065  clwwlknon1nloop  30131  clwwlknon1sn  30132  eupth2lem3lem6  30265  nfrgr2v  30304  1to2vfriswmgr  30311  4cyclusnfrgr  30324  frgrnbnb  30325  frgrncvvdeqlem1  30331  frgrncvvdeqlem7  30337  frgrncvvdeqlem8  30338  frgrncvvdeqlem9  30339  frgrwopreg  30355  frgrregord013  30427  lpni  30512  xrge0iifcnv  33879  0nn0m1nnn0  35080  satf0n0  35346  fmlafvel  35353  fmlaomn0  35358  fmlan0  35359  tailfb  36343  dfac21  43023  dvgrat  44281  cvgdvgrat  44282  rusbcALT  44408  fsetsnprcnex  46970  fsetprcnexALT  46977  aiota0ndef  47012  ndfatafv2nrn  47136  afv2ndefb  47139  dfatafv2rnb  47142  fafv2elrnb  47150  afv2ndeffv0  47175  nelbrnel  47191  nelbrnelim  47192  fvmptrab  47207  readdcnnred  47218  resubcnnred  47219  recnmulnred  47220  cndivrenred  47221  sqrtnegnre  47222  0nelsetpreimafv  47264  spr0nelg  47350  spr0el  47356  prminf2  47462  requad01  47495  0noddALTV  47563  1nevenALTV  47565  2noddALTV  47567  nn0o1gt2ALTV  47568  nn0oALTV  47570  341fppr2  47608  9fppr8  47611  clnbgr0vtx  47708  lidldomnnring  47959  2zrngnring  47981  cznnring  47985  pgrpgt2nabl  48091  lmod1zrnlvec  48223  lvecpsslmod  48236  suppdm  48239  elbigolo1  48291  ifnmfalse  48855  aacllem  48895