Definition df-nel 3038

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

This definition is referenced by:  neli  3039  nelir  3040  nelcon3d  3041  neleq12d  3042  nfnel  3045  nfneld  3046  nnel  3047  elnelne1  3048  elnelne2  3049  pm2.24nel  3050  pm2.61danel  3051  ru  3740  ruOLD  3741  ssexnelpss  4070  raldifb  4103  elneldisj  4346  elnelun  4347  sbcnel12g  4368  elpwdifsn  4747  0nelrel  5695  feldmfvelcdm  7042  f1ounsn  7230  snnex  7715  pwnex  7716  ssonprc  7744  resf1extb  7888  opabn1stprc  8014  mpoxneldm  8166  mpoxopoveqd  8175  undefnel  8232  fsetdmprc0  8806  fsetcdmex  8814  fsetexb  8815  fiprc  8995  funsnfsupp  9309  elnel  9534  noinfep  9583  dfac9  10061  fz0  13469  0nelfz1  13473  nelfzo  13594  fvinim0ffz  13719  injresinjlem  13720  ssnn0fi  13922  hashnnn0genn0  14280  hashnemnf  14281  hashinfxadd  14322  wrdlndm  14467  wrdsymb0  14486  pfxnd0  14626  repsundef  14708  repswswrd  14721  rennim  15176  cnpart  15177  sqrtneglem  15203  sqreulem  15297  eqsqrtd  15305  fsumsplitsnun  15692  modfsummods  15730  sqrt2irr0  16190  sumeven  16328  sumodd  16329  lcmfval  16562  lcmfn0val  16564  lcmfcl  16569  lcmfnncl  16570  lcmfeq0b  16571  dvdslcmf  16572  lcmftp  16577  lcmfunsnlem2lem1  16579  lcmfunsnlem2lem2  16580  lcmfunsnlem2  16581  ncoprmlnprm  16669  prmgaplem5  16997  prmgaplem6  16998  chnfibg  18573  isnsgrp  18662  isnmnd  18677  dprddomprc  19948  dprddomcld  19949  dprdval0prc  19950  dprdsubg  19972  zrninitoringc  20626  rng1nnzr  20725  rng1nfld  20729  islindf4  21810  nfimdetndef  22550  mdetfval1  22551  dfac14  23579  0nelfb  23792  fbun  23801  opnfbas  23803  trfbas2  23804  isfil2  23817  fsubbas  23828  fbasrn  23845  rnelfmlem  23913  tsmsfbas  24089  ustfilxp  24174  metustfbas  24518  iccpnfcnv  24915  zclmncvs  25121  cphsqrtcl2  25159  minveclem3b  25401  2sq2  27417  vtxvalprc  29136  iedgvalprc  29137  umgrnloop2  29237  nbuhgr  29434  nbumgr  29438  uhgrnbgr0nb  29445  nbgr0vtx  29446  nbgr0edglem  29447  nbgr1vtx  29449  nbgrnself  29450  nbgrnself2  29451  nbgrssovtx  29452  nbgrssvwo2  29453  nbupgrres  29455  nbusgrvtxm1  29470  nb3grprlem2  29472  1hevtxdg0  29597  p1evtxdeqlem  29604  rgrx0ndm  29685  wlkreslem  29759  dfpth2  29820  pthdlem2lem  29858  wwlksnfi  29997  clwwlkneq0  30122  clwwlknnn  30126  clwwlknon1nloop  30192  clwwlknon1sn  30193  eupth2lem3lem6  30326  nfrgr2v  30365  1to2vfriswmgr  30372  4cyclusnfrgr  30385  frgrnbnb  30386  frgrncvvdeqlem1  30392  frgrncvvdeqlem7  30398  frgrncvvdeqlem8  30399  frgrncvvdeqlem9  30400  frgrwopreg  30416  frgrregord013  30488  lpni  30574  evlextv  33725  constrsqrtcl  33963  xrge0iifcnv  34117  noinfepfnregs  35316  noinfepregs  35317  0nn0m1nnn0  35335  satf0n0  35600  fmlafvel  35607  fmlaomn0  35612  fmlan0  35613  tailfb  36599  dfac21  43452  dvgrat  44697  cvgdvgrat  44698  rusbcALT  44823  nthrucw  47273  fsetsnprcnex  47444  fsetprcnexALT  47451  aiota0ndef  47486  ndfatafv2nrn  47610  afv2ndefb  47613  dfatafv2rnb  47616  fafv2elrnb  47624  afv2ndeffv0  47649  nelbrnel  47665  nelbrnelim  47666  fvmptrab  47681  readdcnnred  47692  resubcnnred  47693  recnmulnred  47694  cndivrenred  47695  sqrtnegnre  47696  0nelsetpreimafv  47779  spr0nelg  47865  spr0el  47871  prminf2  47977  requad01  48010  0noddALTV  48078  1nevenALTV  48080  2noddALTV  48082  nn0o1gt2ALTV  48083  nn0oALTV  48085  341fppr2  48123  9fppr8  48126  clnbgr0vtx  48225  isubgr3stgrlem3  48357  gpg5nbgrvtx03starlem1  48457  gpg5nbgrvtx03starlem2  48458  gpg5nbgrvtx03starlem3  48459  gpg5nbgrvtx13starlem1  48460  gpg5nbgrvtx13starlem2  48461  gpg5nbgrvtx13starlem3  48462  gpg5nbgrvtx03star  48469  gpg5nbgr3star  48470  lidldomnnring  48625  2zrngnring  48647  cznnring  48651  pgrpgt2nabl  48755  lmod1zrnlvec  48883  lvecpsslmod  48896  suppdm  48899  elbigolo1  48946  ifnmfalse  50151  aacllem  50189