Definition df-nel 3063

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

This definition is referenced by:  neli  3064  nelir  3065  nelcon3d  3066  neleq12d  3067  nfnel  3070  nfneld  3071  nnel  3072  elnelne1  3073  elnelne2  3074  pm2.24nel  3075  pm2.61danel  3076  ru  3742  ssexnelpss  4070  raldifb  4102  elneldisj  4348  elnelun  4349  sbcnel12g  4378  elpwdifsn  4756  0nelrel  5722  feldmfvelcdm  7081  f1ounsn  7270  snnex  7756  pwnex  7757  ssonprc  7785  resf1extb  7930  opabn1stprc  8054  mpoxneldm  8207  mpoxopoveqd  8216  undefnel  8274  fsetdmprc0  8851  fsetcdmex  8859  fsetexb  8860  fiprc  9040  funsnfsupp  9351  elnel  9579  noinfep  9628  dfac9  10119  fz0  13566  0nelfz1  13570  nelfzo  13692  fvinim0ffz  13817  injresinjlem  13818  ssnn0fi  14020  hashnnn0genn0  14378  hashnemnf  14379  hashinfxadd  14420  wrdlndm  14566  wrdsymb0  14585  pfxnd0  14725  repsundef  14807  repswswrd  14820  rennim  15289  cnpart  15290  sqrtneglem  15316  sqreulem  15410  eqsqrtd  15418  fsumsplitsnun  15805  modfsummods  15844  sqrt2irr0  16306  sumeven  16444  sumodd  16445  lcmfval  16678  lcmfn0val  16680  lcmfcl  16685  lcmfnncl  16686  lcmfeq0b  16687  dvdslcmf  16688  lcmftp  16693  lcmfunsnlem2lem1  16695  lcmfunsnlem2lem2  16696  lcmfunsnlem2  16697  ncoprmlnprm  16786  prmgaplem5  17114  prmgaplem6  17115  chnfibg  18691  isnsgrp  18780  isnmnd  18795  dprddomprc  20071  dprddomcld  20072  dprdval0prc  20073  dprdsubg  20095  zrninitoringc  20760  rng1nnzr  20858  rng1nfld  20861  islindf4  21967  nfimdetndef  22725  mdetfval1  22726  dfac14  23754  0nelfb  23967  fbun  23976  opnfbas  23978  trfbas2  23979  isfil2  23992  fsubbas  24003  fbasrn  24020  rnelfmlem  24088  tsmsfbas  24264  ustfilxp  24349  metustfbas  24693  iccpnfcnv  25082  zclmncvs  25286  cphsqrtcl2  25324  minveclem3b  25566  2sq2  27573  vtxvalprc  29361  iedgvalprc  29362  umgrnloop2  29462  nbuhgr  29659  nbumgr  29663  uhgrnbgr0nb  29670  nbgr0vtx  29671  nbgr0edglem  29672  nbgr1vtx  29674  nbgrnself  29675  nbgrnself2  29676  nbgrssovtx  29677  nbgrssvwo2  29678  nbupgrres  29680  nbusgrvtxm1  29695  nb3grprlem2  29697  1hevtxdg0  29821  p1evtxdeqlem  29828  rgrx0ndm  29909  wlkreslem  29983  dfpth2  30044  pthdlem2lem  30082  wwlksnfi  30221  clwwlkneq0  30346  clwwlknnn  30350  clwwlknon1nloop  30416  clwwlknon1sn  30417  eupth2lem3lem6  30550  nfrgr2v  30589  1to2vfriswmgr  30596  4cyclusnfrgr  30609  frgrnbnb  30610  frgrncvvdeqlem1  30616  frgrncvvdeqlem7  30622  frgrncvvdeqlem8  30623  frgrncvvdeqlem9  30624  frgrwopreg  30640  frgrregord013  30712  lpni  30798  evlextv  33898  constrsqrtcl  34135  xrge0iifcnv  34289  noinfepfnregs  35499  noinfepregs  35500  0nn0m1nnn0  35558  satf0n0  35824  fmlafvel  35831  fmlaomn0  35836  fmlan0  35837  tailfb  36832  dfac21  43741  dvgrat  44970  cvgdvgrat  44971  rusbcALT  45096  nthrucw  47550  fsetsnprcnex  47737  fsetprcnexALT  47744  aiota0ndef  47779  ndfatafv2nrn  47903  afv2ndefb  47906  dfatafv2rnb  47909  fafv2elrnb  47917  afv2ndeffv0  47942  nelbrnel  47958  nelbrnelim  47959  fvmptrab  47974  readdcnnred  47985  resubcnnred  47986  recnmulnred  47987  cndivrenred  47988  sqrtnegnre  47989  0nelsetpreimafv  48084  spr0nelg  48170  spr0el  48176  prminf2  48285  indprm  48326  indprmfz  48327  requad01  48331  0noddALTV  48399  1nevenALTV  48401  2noddALTV  48403  nn0o1gt2ALTV  48404  nn0oALTV  48406  341fppr2  48444  9fppr8  48447  clnbgr0vtx  48546  isubgr3stgrlem3  48678  gpg5nbgrvtx03starlem1  48778  gpg5nbgrvtx03starlem2  48779  gpg5nbgrvtx03starlem3  48780  gpg5nbgrvtx13starlem1  48781  gpg5nbgrvtx13starlem2  48782  gpg5nbgrvtx13starlem3  48783  gpg5nbgrvtx03star  48790  gpg5nbgr3star  48791  lidldomnnring  48946  2zrngnring  48968  cznnring  48972  pgrpgt2nabl  49091  lmod1zrnlvec  49219  lvecpsslmod  49232  suppdm  49235  elbigolo1  49282  ifnmfalse  50486  aacllem  50546