Definition df-nel 3064

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

This definition is referenced by:  neli  3065  nelir  3066  nelcon3d  3067  neleq12d  3068  nfnel  3071  nfneld  3072  nnel  3073  elnelne1  3074  elnelne2  3075  pm2.24nel  3076  pm2.61danel  3077  ru  3745  ssexnelpss  4072  raldifb  4104  elneldisj  4348  elnelun  4349  sbcnel12g  4370  elpwdifsn  4751  0nelrel  5710  feldmfvelcdm  7069  f1ounsn  7258  snnex  7743  pwnex  7744  ssonprc  7772  resf1extb  7917  opabn1stprc  8041  mpoxneldm  8194  mpoxopoveqd  8203  undefnel  8261  fsetdmprc0  8838  fsetcdmex  8846  fsetexb  8847  fiprc  9027  funsnfsupp  9340  elnel  9568  noinfep  9617  dfac9  10095  fz0  13546  0nelfz1  13550  nelfzo  13672  fvinim0ffz  13797  injresinjlem  13798  ssnn0fi  14000  hashnnn0genn0  14358  hashnemnf  14359  hashinfxadd  14400  wrdlndm  14545  wrdsymb0  14564  pfxnd0  14704  repsundef  14786  repswswrd  14799  rennim  15268  cnpart  15269  sqrtneglem  15295  sqreulem  15389  eqsqrtd  15397  fsumsplitsnun  15784  modfsummods  15823  sqrt2irr0  16285  sumeven  16423  sumodd  16424  lcmfval  16657  lcmfn0val  16659  lcmfcl  16664  lcmfnncl  16665  lcmfeq0b  16666  dvdslcmf  16667  lcmftp  16672  lcmfunsnlem2lem1  16674  lcmfunsnlem2lem2  16675  lcmfunsnlem2  16676  ncoprmlnprm  16765  prmgaplem5  17093  prmgaplem6  17094  chnfibg  18670  isnsgrp  18759  isnmnd  18774  dprddomprc  20044  dprddomcld  20045  dprdval0prc  20046  dprdsubg  20068  zrninitoringc  20728  rng1nnzr  20827  rng1nfld  20830  islindf4  21892  nfimdetndef  22651  mdetfval1  22652  dfac14  23680  0nelfb  23893  fbun  23902  opnfbas  23904  trfbas2  23905  isfil2  23918  fsubbas  23929  fbasrn  23946  rnelfmlem  24014  tsmsfbas  24190  ustfilxp  24275  metustfbas  24619  iccpnfcnv  25008  zclmncvs  25212  cphsqrtcl2  25250  minveclem3b  25492  2sq2  27499  vtxvalprc  29248  iedgvalprc  29249  umgrnloop2  29349  nbuhgr  29546  nbumgr  29550  uhgrnbgr0nb  29557  nbgr0vtx  29558  nbgr0edglem  29559  nbgr1vtx  29561  nbgrnself  29562  nbgrnself2  29563  nbgrssovtx  29564  nbgrssvwo2  29565  nbupgrres  29567  nbusgrvtxm1  29582  nb3grprlem2  29584  1hevtxdg0  29708  p1evtxdeqlem  29715  rgrx0ndm  29796  wlkreslem  29870  dfpth2  29931  pthdlem2lem  29969  wwlksnfi  30108  clwwlkneq0  30233  clwwlknnn  30237  clwwlknon1nloop  30303  clwwlknon1sn  30304  eupth2lem3lem6  30437  nfrgr2v  30476  1to2vfriswmgr  30483  4cyclusnfrgr  30496  frgrnbnb  30497  frgrncvvdeqlem1  30503  frgrncvvdeqlem7  30509  frgrncvvdeqlem8  30510  frgrncvvdeqlem9  30511  frgrwopreg  30527  frgrregord013  30599  lpni  30685  evlextv  33841  constrsqrtcl  34078  xrge0iifcnv  34232  noinfepfnregs  35432  noinfepregs  35433  0nn0m1nnn0  35467  satf0n0  35733  fmlafvel  35740  fmlaomn0  35745  fmlan0  35746  tailfb  36742  dfac21  43648  dvgrat  44893  cvgdvgrat  44894  rusbcALT  45019  nthrucw  47467  fsetsnprcnex  47654  fsetprcnexALT  47661  aiota0ndef  47696  ndfatafv2nrn  47820  afv2ndefb  47823  dfatafv2rnb  47826  fafv2elrnb  47834  afv2ndeffv0  47859  nelbrnel  47875  nelbrnelim  47876  fvmptrab  47891  readdcnnred  47902  resubcnnred  47903  recnmulnred  47904  cndivrenred  47905  sqrtnegnre  47906  0nelsetpreimafv  48001  spr0nelg  48087  spr0el  48093  prminf2  48202  indprm  48243  indprmfz  48244  requad01  48248  0noddALTV  48316  1nevenALTV  48318  2noddALTV  48320  nn0o1gt2ALTV  48321  nn0oALTV  48323  341fppr2  48361  9fppr8  48364  clnbgr0vtx  48463  isubgr3stgrlem3  48595  gpg5nbgrvtx03starlem1  48695  gpg5nbgrvtx03starlem2  48696  gpg5nbgrvtx03starlem3  48697  gpg5nbgrvtx13starlem1  48698  gpg5nbgrvtx13starlem2  48699  gpg5nbgrvtx13starlem3  48700  gpg5nbgrvtx03star  48707  gpg5nbgr3star  48708  lidldomnnring  48863  2zrngnring  48885  cznnring  48889  pgrpgt2nabl  48993  lmod1zrnlvec  49121  lvecpsslmod  49134  suppdm  49137  elbigolo1  49184  ifnmfalse  50389  aacllem  50427