Definition df-nel 3050

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

This definition is referenced by:  neli  3051  nelir  3052  neleq12d  3053  nfnel  3056  nfneld  3057  nnel  3058  elnelne1  3059  elnelne2  3060  nelcon3d  3061  elnelall  3062  pm2.61danel  3063  ru  3715  ssexnelpss  4048  raldifb  4079  elneldisj  4322  elnelun  4323  sbcnel12g  4345  elpwdifsn  4722  0nelrel  5648  snnex  7608  pwnex  7609  ssonprc  7637  opabn1stprc  7898  mpoxneldm  8028  mpoxopoveqd  8037  undefnel  8094  fsetdmprc0  8643  fsetcdmex  8651  fsetexb  8652  fiprc  8835  funsnfsupp  9152  elnel  9369  noinfep  9418  dfac9  9892  fz0  13271  0nelfz1  13275  nelfzo  13392  fvinim0ffz  13506  injresinjlem  13507  ssnn0fi  13705  hashnnn0genn0  14057  hashnemnf  14058  hashinfxadd  14100  wrdlndm  14233  wrdsymb0  14252  pfxnd0  14401  repsundef  14484  repswswrd  14497  rennim  14950  cnpart  14951  sqrtneglem  14978  sqreulem  15071  eqsqrtd  15079  fsumsplitsnun  15467  modfsummods  15505  sqrt2irr0  15960  sumeven  16096  sumodd  16097  lcmfval  16326  lcmfn0val  16328  lcmfcl  16333  lcmfnncl  16334  lcmfeq0b  16335  dvdslcmf  16336  lcmftp  16341  lcmfunsnlem2lem1  16343  lcmfunsnlem2lem2  16344  lcmfunsnlem2  16345  ncoprmlnprm  16432  prmgaplem5  16756  prmgaplem6  16757  isnsgrp  18379  isnmnd  18389  dprddomprc  19603  dprddomcld  19604  dprdval0prc  19605  dprdsubg  19627  rng1nnzr  20545  rng1nfld  20549  islindf4  21045  nfimdetndef  21738  mdetfval1  21739  dfac14  22769  0nelfb  22982  fbun  22991  opnfbas  22993  trfbas2  22994  isfil2  23007  fsubbas  23018  fbasrn  23035  rnelfmlem  23103  tsmsfbas  23279  ustfilxp  23364  metustfbas  23713  iccpnfcnv  24107  zclmncvs  24312  cphsqrtcl2  24350  minveclem3b  24592  2sq2  26581  vtxvalprc  27415  iedgvalprc  27416  umgrnloop2  27516  nbuhgr  27710  nbumgr  27714  uhgrnbgr0nb  27721  nbgr0vtxlem  27722  nbgr1vtx  27725  nbgrnself  27726  nbgrnself2  27727  nbgrssovtx  27728  nbgrssvwo2  27729  nbupgrres  27731  nbusgrvtxm1  27746  nb3grprlem2  27748  1hevtxdg0  27872  p1evtxdeqlem  27879  rgrx0ndm  27960  wlkreslem  28037  pthdlem2lem  28135  wwlksnfi  28271  clwwlkneq0  28393  clwwlknnn  28397  clwwlknon1nloop  28463  clwwlknon1sn  28464  eupth2lem3lem6  28597  nfrgr2v  28636  1to2vfriswmgr  28643  4cyclusnfrgr  28656  frgrnbnb  28657  frgrncvvdeqlem1  28663  frgrncvvdeqlem7  28669  frgrncvvdeqlem8  28670  frgrncvvdeqlem9  28671  frgrwopreg  28687  frgrregord013  28759  lpni  28842  xrge0iifcnv  31883  0nn0m1nnn0  33071  satf0n0  33340  fmlafvel  33347  fmlaomn0  33352  fmlan0  33353  tailfb  34566  dfac21  40891  dvgrat  41930  cvgdvgrat  41931  rusbcALT  42057  fsetsnprcnex  44549  fsetprcnexALT  44556  aiota0ndef  44589  ndfatafv2nrn  44713  afv2ndefb  44716  dfatafv2rnb  44719  fafv2elrnb  44727  afv2ndeffv0  44752  nelbrnel  44768  nelbrnelim  44769  fvmptrab  44784  readdcnnred  44795  resubcnnred  44796  recnmulnred  44797  cndivrenred  44798  sqrtnegnre  44799  0nelsetpreimafv  44842  spr0nelg  44928  spr0el  44934  prminf2  45040  requad01  45073  0noddALTV  45141  1nevenALTV  45143  2noddALTV  45145  nn0o1gt2ALTV  45146  nn0oALTV  45148  341fppr2  45186  9fppr8  45189  lidldomnnring  45488  2zrngnring  45510  cznnring  45514  zrninitoringc  45629  pgrpgt2nabl  45702  lmod1zrnlvec  45835  lvecpsslmod  45848  suppdm  45851  elbigolo1  45903  ifnmfalse  46465  aacllem  46505