Definition df-nel 3039

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

This definition is referenced by:  neli  3040  nelir  3041  nelcon3d  3042  neleq12d  3043  nfnel  3046  nfneld  3047  nnel  3048  elnelne1  3049  elnelne2  3050  pm2.24nel  3051  pm2.61danel  3052  ru  3768  ssexnelpss  4105  raldifb  4136  elneldisj  4380  elnelun  4381  sbcnel12g  4403  elpwdifsn  4784  0nelrel  5727  snnex  7738  pwnex  7739  ssonprc  7768  opabn1stprc  8037  mpoxneldm  8192  mpoxopoveqd  8201  undefnel  8258  fsetdmprc0  8845  fsetcdmex  8853  fsetexb  8854  fiprc  9041  funsnfsupp  9383  elnel  9602  noinfep  9651  dfac9  10127  fz0  13513  0nelfz1  13517  nelfzo  13634  fvinim0ffz  13748  injresinjlem  13749  ssnn0fi  13947  hashnnn0genn0  14300  hashnemnf  14301  hashinfxadd  14342  wrdlndm  14477  wrdsymb0  14496  pfxnd0  14635  repsundef  14718  repswswrd  14731  rennim  15183  cnpart  15184  sqrtneglem  15210  sqreulem  15303  eqsqrtd  15311  fsumsplitsnun  15698  modfsummods  15736  sqrt2irr0  16191  sumeven  16327  sumodd  16328  lcmfval  16555  lcmfn0val  16557  lcmfcl  16562  lcmfnncl  16563  lcmfeq0b  16564  dvdslcmf  16565  lcmftp  16570  lcmfunsnlem2lem1  16572  lcmfunsnlem2lem2  16573  lcmfunsnlem2  16574  ncoprmlnprm  16663  prmgaplem5  16987  prmgaplem6  16988  isnsgrp  18646  isnmnd  18661  dprddomprc  19912  dprddomcld  19913  dprdval0prc  19914  dprdsubg  19936  zrninitoringc  20562  rng1nnzr  20616  rng1nfld  20620  islindf4  21701  nfimdetndef  22413  mdetfval1  22414  dfac14  23444  0nelfb  23657  fbun  23666  opnfbas  23668  trfbas2  23669  isfil2  23682  fsubbas  23693  fbasrn  23710  rnelfmlem  23778  tsmsfbas  23954  ustfilxp  24039  metustfbas  24388  iccpnfcnv  24791  zclmncvs  24998  cphsqrtcl2  25036  minveclem3b  25278  2sq2  27282  vtxvalprc  28774  iedgvalprc  28775  umgrnloop2  28875  nbuhgr  29069  nbumgr  29073  uhgrnbgr0nb  29080  nbgr0vtxlem  29081  nbgr1vtx  29084  nbgrnself  29085  nbgrnself2  29086  nbgrssovtx  29087  nbgrssvwo2  29088  nbupgrres  29090  nbusgrvtxm1  29105  nb3grprlem2  29107  1hevtxdg0  29231  p1evtxdeqlem  29238  rgrx0ndm  29319  wlkreslem  29395  pthdlem2lem  29493  wwlksnfi  29629  clwwlkneq0  29751  clwwlknnn  29755  clwwlknon1nloop  29821  clwwlknon1sn  29822  eupth2lem3lem6  29955  nfrgr2v  29994  1to2vfriswmgr  30001  4cyclusnfrgr  30014  frgrnbnb  30015  frgrncvvdeqlem1  30021  frgrncvvdeqlem7  30027  frgrncvvdeqlem8  30028  frgrncvvdeqlem9  30029  frgrwopreg  30045  frgrregord013  30117  lpni  30202  xrge0iifcnv  33402  0nn0m1nnn0  34591  satf0n0  34858  fmlafvel  34865  fmlaomn0  34870  fmlan0  34871  tailfb  35752  dfac21  42297  dvgrat  43560  cvgdvgrat  43561  rusbcALT  43687  fsetsnprcnex  46250  fsetprcnexALT  46257  aiota0ndef  46290  ndfatafv2nrn  46414  afv2ndefb  46417  dfatafv2rnb  46420  fafv2elrnb  46428  afv2ndeffv0  46453  nelbrnel  46469  nelbrnelim  46470  fvmptrab  46485  readdcnnred  46496  resubcnnred  46497  recnmulnred  46498  cndivrenred  46499  sqrtnegnre  46500  0nelsetpreimafv  46543  spr0nelg  46629  spr0el  46635  prminf2  46741  requad01  46774  0noddALTV  46842  1nevenALTV  46844  2noddALTV  46846  nn0o1gt2ALTV  46847  nn0oALTV  46849  341fppr2  46887  9fppr8  46890  lidldomnnring  47099  2zrngnring  47121  cznnring  47125  pgrpgt2nabl  47231  lmod1zrnlvec  47363  lvecpsslmod  47376  suppdm  47379  elbigolo1  47431  ifnmfalse  47996  aacllem  48036