Definition df-nel 3062

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

This definition is used by:  neli  3063  nelir  3064  nelcon3d  3065  neleq12d  3066  nfnel  3069  nfneld  3070  nnel  3071  elnelne1  3072  elnelne2  3073  pm2.24nel  3074  pm2.61danel  3075  ru  3737  ssexnelpss  4044  raldifb  4085  elneldisj  4341  elnelun  4342  sbcnel12g  4371  elpwdifsn  4751  0nelrel  5711  feldmfvelcdm  7086  f1ounsn  7280  snnex  7772  pwnex  7773  ssonprc  7801  resf1extb  7946  opabn1stprc  8069  mpoxneldm  8229  mpoxopoveqd  8238  undefnel  8296  fsetdmprc0  8877  fsetcdmex  8885  fsetexb  8886  fiprc  9072  funsnfsupp  9384  elnel  9612  noinfep  9661  dfac9  10215  0nn0m1nnn0  12753  fz0  13672  0nelfz1  13676  nelfzo  13799  fvinim0ffz  13924  injresinjlem  13925  ssnn0fi  14128  hashnnn0genn0  14487  hashnemnf  14488  hashinfxadd  14529  wrdlndm  14675  wrdsymb0  14694  pfxnd0  14838  repsundef  14922  repswswrd  14935  rennim  15406  cnpart  15407  sqrtneglem  15433  sqreulem  15527  eqsqrtd  15535  fsumsplitsnun  15921  modfsummods  15960  sqrt2irr0  16419  sumeven  16557  sumodd  16558  lcmfval  16796  lcmfn0val  16798  lcmfcl  16803  lcmfnncl  16804  lcmfeq0b  16805  dvdslcmf  16806  lcmftp  16811  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  lcmfunsnlem2  16815  ncoprmlnprm  16904  prmgaplem5  17233  prmgaplem6  17234  chnfibg  18810  mgmn0plusgf  18827  isnsgrp  18912  isnmnd  18927  dprddomprc  20216  dprddomcld  20217  dprdval0prc  20218  dprdsubg  20240  zrninitoringc  20928  rng1nnzr  21033  rng1nfld  21036  islindf4  22144  nfimdetndef  22904  mdetfval1  22905  dfac14  23937  0nelfb  24150  fbun  24159  opnfbas  24161  trfbas2  24162  isfil2  24175  fsubbas  24186  fbasrn  24203  rnelfmlem  24271  tsmsfbas  24447  ustfilxp  24532  metustfbas  24876  iccpnfcnv  25265  zclmncvs  25469  cphsqrtcl2  25507  minveclem3b  25749  2sq2  27760  vtxvalprc  29623  iedgvalprc  29624  umgrnloop2  29724  nbuhgr  29924  nbumgr  29928  uhgrnbgr0nb  29935  nbgr0vtx  29936  nbgr0edglem  29937  nbgr1vtx  29939  nbgrnself  29940  nbgrnself2  29941  nbgrssovtx  29942  nbgrssvwo2  29943  nbupgrres  29945  nbusgrvtxm1  29960  nb3grprlem2  29962  1hevtxdg0  30086  p1evtxdeqlem  30093  rgrx0ndm  30174  wlkreslem  30248  dfpth2  30314  pthdlem2lem  30353  wwlksnfi  30495  clwwlkneq0  30620  clwwlknnn  30624  clwwlknon1nloop  30690  clwwlknon1sn  30691  eupth2lem3lem6  30834  nfrgr2v  30873  1to2vfriswmgr  30880  4cyclusnfrgr  30893  frgrnbnb  30894  frgrncvvdeqlem1  30900  frgrncvvdeqlem7  30906  frgrncvvdeqlem8  30907  frgrncvvdeqlem9  30908  frgrwopreg  30924  frgrregord013  30996  lpni  31082  evlextv  34216  constrsqrtcl  34453  xrge0iifcnv  34607  noinfepfnregs  35842  noinfepregs  35843  satf0n0  36185  fmlafvel  36192  fmlaomn0  36197  fmlan0  36198  tailfb  37207  dfac21  44110  dvgrat  45338  cvgdvgrat  45339  rusbcALT  45464  fsetsnprcnex  48167  fsetprcnexALT  48174  aiota0ndef  48209  ndfatafv2nrn  48333  afv2ndefb  48336  dfatafv2rnb  48339  fafv2elrnb  48347  afv2ndeffv0  48372  nelbrnel  48388  nelbrnelim  48389  fvmptrab  48404  readdcnnred  48415  resubcnnred  48416  recnmulnred  48417  cndivrenred  48418  sqrtnegnre  48419  0nelsetpreimafv  48514  spr0nelg  48600  spr0el  48606  prminf2  48715  indprm  48756  indprmfz  48757  requad01  48761  0noddALTV  48829  1nevenALTV  48831  2noddALTV  48833  nn0o1gt2ALTV  48834  nn0oALTV  48836  341fppr2  48874  9fppr8  48877  clnbgr0vtx  48976  isubgr3stgrlem3  49108  gpg5nbgrvtx03starlem1  49208  gpg5nbgrvtx03starlem2  49209  gpg5nbgrvtx03starlem3  49210  gpg5nbgrvtx13starlem1  49211  gpg5nbgrvtx13starlem2  49212  gpg5nbgrvtx13starlem3  49213  gpg5nbgrvtx03star  49220  gpg5nbgr3star  49221  lidldomnnring  49375  2zrngnring  49397  cznnring  49401  pgrpgt2nabl  49520  lmod1zrnlvec  49648  lvecpsslmod  49661  suppdm  49664  elbigolo1  49711  ifnmfalse  50901  aacllem  50981