Definition df-nel 3044

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

This definition is referenced by:  neli  3045  nelir  3046  nelcon3d  3047  neleq12d  3048  nfnel  3051  nfneld  3052  nnel  3053  elnelne1  3054  elnelne2  3055  pm2.24nel  3056  pm2.61danel  3057  ru  3788  ruOLD  3789  ssexnelpss  4125  raldifb  4158  elneldisj  4397  elnelun  4398  sbcnel12g  4419  elpwdifsn  4793  0nelrel  5749  feldmfvelcdm  7105  f1ounsn  7291  snnex  7776  pwnex  7777  ssonprc  7806  opabn1stprc  8081  mpoxneldm  8235  mpoxopoveqd  8244  undefnel  8301  fsetdmprc0  8893  fsetcdmex  8901  fsetexb  8902  fiprc  9083  funsnfsupp  9429  elnel  9648  noinfep  9697  dfac9  10174  fz0  13575  0nelfz1  13579  nelfzo  13700  fvinim0ffz  13821  injresinjlem  13822  ssnn0fi  14022  hashnnn0genn0  14378  hashnemnf  14379  hashinfxadd  14420  wrdlndm  14564  wrdsymb0  14583  pfxnd0  14722  repsundef  14805  repswswrd  14818  rennim  15274  cnpart  15275  sqrtneglem  15301  sqreulem  15394  eqsqrtd  15402  fsumsplitsnun  15787  modfsummods  15825  sqrt2irr0  16283  sumeven  16420  sumodd  16421  lcmfval  16654  lcmfn0val  16656  lcmfcl  16661  lcmfnncl  16662  lcmfeq0b  16663  dvdslcmf  16664  lcmftp  16669  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  ncoprmlnprm  16761  prmgaplem5  17088  prmgaplem6  17089  isnsgrp  18748  isnmnd  18763  dprddomprc  20034  dprddomcld  20035  dprdval0prc  20036  dprdsubg  20058  zrninitoringc  20692  rng1nnzr  20792  rng1nfld  20796  islindf4  21875  nfimdetndef  22610  mdetfval1  22611  dfac14  23641  0nelfb  23854  fbun  23863  opnfbas  23865  trfbas2  23866  isfil2  23879  fsubbas  23890  fbasrn  23907  rnelfmlem  23975  tsmsfbas  24151  ustfilxp  24236  metustfbas  24585  iccpnfcnv  24988  zclmncvs  25195  cphsqrtcl2  25233  minveclem3b  25475  2sq2  27491  vtxvalprc  29076  iedgvalprc  29077  umgrnloop2  29177  nbuhgr  29374  nbumgr  29378  uhgrnbgr0nb  29385  nbgr0vtx  29386  nbgr0edglem  29387  nbgr1vtx  29389  nbgrnself  29390  nbgrnself2  29391  nbgrssovtx  29392  nbgrssvwo2  29393  nbupgrres  29395  nbusgrvtxm1  29410  nb3grprlem2  29412  1hevtxdg0  29537  p1evtxdeqlem  29544  rgrx0ndm  29625  wlkreslem  29701  pthdlem2lem  29799  wwlksnfi  29935  clwwlkneq0  30057  clwwlknnn  30061  clwwlknon1nloop  30127  clwwlknon1sn  30128  eupth2lem3lem6  30261  nfrgr2v  30300  1to2vfriswmgr  30307  4cyclusnfrgr  30320  frgrnbnb  30321  frgrncvvdeqlem1  30327  frgrncvvdeqlem7  30333  frgrncvvdeqlem8  30334  frgrncvvdeqlem9  30335  frgrwopreg  30351  frgrregord013  30423  lpni  30508  xrge0iifcnv  33893  0nn0m1nnn0  35096  satf0n0  35362  fmlafvel  35369  fmlaomn0  35374  fmlan0  35375  tailfb  36359  dfac21  43054  dvgrat  44307  cvgdvgrat  44308  rusbcALT  44434  fsetsnprcnex  47004  fsetprcnexALT  47011  aiota0ndef  47046  ndfatafv2nrn  47170  afv2ndefb  47173  dfatafv2rnb  47176  fafv2elrnb  47184  afv2ndeffv0  47209  nelbrnel  47225  nelbrnelim  47226  fvmptrab  47241  readdcnnred  47252  resubcnnred  47253  recnmulnred  47254  cndivrenred  47255  sqrtnegnre  47256  0nelsetpreimafv  47314  spr0nelg  47400  spr0el  47406  prminf2  47512  requad01  47545  0noddALTV  47613  1nevenALTV  47615  2noddALTV  47617  nn0o1gt2ALTV  47618  nn0oALTV  47620  341fppr2  47658  9fppr8  47661  clnbgr0vtx  47759  isubgr3stgrlem3  47870  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  lidldomnnring  48079  2zrngnring  48101  cznnring  48105  pgrpgt2nabl  48210  lmod1zrnlvec  48339  lvecpsslmod  48352  suppdm  48355  elbigolo1  48406  ifnmfalse  48993  aacllem  49031