Theorem eldifsn 4730

Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)

Assertion

Ref	Expression
eldifsn	⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Proof of Theorem eldifsn

Step	Hyp	Ref	Expression
1		eldif 3900	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4582	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2970	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 574	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 275	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   ≠ wne 2933   ∖ cdif 3887  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-sn 4569

This theorem is referenced by:  eldifsnd  4731  elpwdifsn  4733  eldifsni  4734  rexdifsn  4738  raldifsni  4739  eldifvsn  4741  difsn  4742  sossfld  6142  tpres  7147  onmindif2  7752  xpord3pred  8093  xpord3inddlem  8095  mptsuppd  8128  suppssr  8136  suppssov1  8138  suppssov2  8139  suppsssn  8142  suppssfv  8143  dif1o  8426  difsnen  8988  limenpsi  9081  frfi  9186  fofinf1o  9233  en2eleq  9919  en2other2  9920  dfac8clem  9943  acni2  9957  acndom  9962  acnnum  9963  dfac9  10048  dfacacn  10053  kmlem3  10064  kmlem4  10065  fin23lem21  10250  canthp1lem2  10565  elni  10788  mulnzcnf  11784  divval  11799  elnnne0  12416  elq  12864  rpcndif0  12927  modfzo0difsn  13867  modsumfzodifsn  13868  expcl2lem  13997  expclzlem  14007  hashdifpr  14339  hashgt23el  14348  prprrab  14397  hashle2prv  14402  reccn2  15521  rlimdiv  15570  eff2  16025  tanval  16054  rpnnen2lem9  16148  fzo0dvdseq  16251  oddprmgt2  16627  oddprmdvds  16832  4sqlem19  16892  prmlem0  17034  prmlem1a  17035  setsnid  17136  grpinvnzcl  18945  symgextf  19350  f1omvdmvd  19376  pmtrprfv  19386  odcau  19537  efgsf  19662  efgsrel  19667  efgs1  19668  efgs1b  19669  efgsp1  19670  efgsres  19671  efgredlema  19673  efgredlemd  19677  efgrelexlemb  19683  gsumpt  19895  dmdprdd  19934  dprdcntz  19943  dprdfeq0  19957  dprd2da  19977  isdomn2OLD  20647  domnrrg  20648  isdomn3  20650  drngunit  20669  isdrng2  20678  drngmcl  20685  drngid2  20687  isdrngd  20700  isdrngdOLD  20702  issubdrg  20715  sdrgacs  20736  cntzsdrg  20737  islss  20887  lssneln0  20906  lssssr  20907  lbsind  21034  lbspss  21036  lspabs3  21078  lspsneq  21079  lspfixed  21085  lspexch  21086  islbs2  21111  cnflddivOLD  21358  cnfldinv  21359  cnsubdrglem  21375  cnmgpid  21386  cnmsubglem  21387  gzrngunit  21390  xrs1mnd  21397  xrs10  21398  xrge0subm  21400  zringunit  21423  zringndrg  21425  domnchr  21489  cnmsgngrp  21536  psgninv  21539  psgndiflemB  21557  lindfind  21773  lindsind  21774  lindff1  21777  lindfrn  21778  mvrcl  21948  coe1tmmul2  22219  mdetunilem9  22563  maducoeval2  22583  gsummatr01lem4  22601  ist1-2  23290  cmpfi  23351  2ndcdisj  23399  2ndcsep  23402  locfincmp  23469  alexsublem  23987  cldsubg  24054  imasdsf1olem  24316  prdsxmslem2  24472  reperflem  24762  xrge0gsumle  24777  xrge0tsms  24778  divcn  24813  evth  24904  cvsdiv  25077  cvsdivcl  25078  cphreccllem  25123  bcthlem5  25273  itg11  25636  i1fmullem  25639  i1fadd  25640  itg1addlem2  25642  i1fmulc  25648  itg1mulc  25649  ellimc3  25824  limcmpt2  25829  dvlem  25841  dvidlem  25860  dvcnp  25864  dvcobr  25891  dvrec  25900  dvrecg  25918  dvmptdiv  25919  dvcnvlem  25921  dvexp3  25923  dveflem  25924  dvferm1lem  25929  dvferm2lem  25931  lhop1lem  25959  ftc1lem5  25988  mdegleb  26010  coe1mul3  26045  ply1nz  26068  fta1blem  26117  fta1b  26118  ig1peu  26121  ig1pdvds  26126  plyeq0lem  26156  dgrub  26180  quotval  26240  fta1lem  26255  fta1  26256  elqaalem3  26269  qaa  26271  iaa  26273  aareccl  26274  aannenlem2  26277  abelthlem8  26389  abelth  26391  eff1olem  26497  logrncl  26516  eflog  26525  logeftb  26532  logdmss  26591  dvlog  26600  logbcl  26717  logbid1  26718  logb1  26719  elogb  26720  logbchbase  26721  relogbval  26722  relogbcl  26723  relogbreexp  26725  relogbmul  26727  nnlogbexp  26731  relogbcxp  26735  cxplogb  26736  relogbcxpb  26737  logbf  26739  logblog  26742  2logb9irrALT  26748  sqrt2cxp2logb9e3  26749  angval  26751  dcubic  26796  rlimcnp  26915  efrlim  26919  efrlimOLD  26920  logexprlim  27176  dchrghm  27207  dchrabs  27211  lgsfcl2  27254  lgsval2lem  27258  lgsval3  27266  lgsmod  27274  lgsdirprm  27282  lgsne0  27286  gausslemma2dlem0f  27312  lgsquad2lem2  27336  2lgsoddprm  27367  2sqlem11  27380  2sqblem  27382  dchrvmaeq0  27455  rpvmasum2  27463  dchrisum0re  27464  qrngdiv  27575  addsval  27942  divsval  28169  elnns  28320  1nns  28329  tglngval  28607  tgisline  28683  axlowdimlem9  29007  axlowdimlem12  29010  axlowdimlem13  29011  elntg2  29042  upgrbi  29150  upgr1elem  29169  umgrislfupgrlem  29179  edgupgr  29191  subgruhgredgd  29341  upgrreslem  29361  nbgrel  29397  nbupgr  29401  nbupgrel  29402  nbumgrvtx  29403  nbgrssovtx  29418  nbupgrres  29421  nbusgrvtxm1uvtx  29462  nbupgruvtxres  29464  iscplgredg  29474  cusgredg  29481  cusgrfilem2  29514  usgredgsscusgredg  29517  1loopgrnb0  29560  1egrvtxdg0  29569  uhgrvd00  29592  vtxdginducedm1lem4  29600  eupth2lem3lem3  30289  frcond1  30325  frcond4  30329  2pthfrgr  30343  3cyclfrgrrn1  30344  n4cyclfrgr  30350  frgrwopreglem4a  30369  numclwwlk5  30447  ressupprn  32752  suppss3  32785  xdivval  32983  xrge0tsmsd  33139  pmtrcnel  33155  pmtrcnelor  33157  0nellinds  33435  dvdsruasso  33450  mxidlirredi  33536  extdg1id  33816  irngnzply1  33841  submatminr1  33960  ordtconnlem1  34074  ispisys2  34303  sigapisys  34305  sibfinima  34489  sseqf  34542  signswch  34711  signstfvn  34719  signsvtn0  34720  signstfvneq0  34722  signstfvcl  34723  signstfveq0a  34726  signstfveq0  34727  signsvfn  34732  signsvtp  34733  signsvtn  34734  signsvfpn  34735  signsvfnn  34736  signlem0  34737  bnj158  34878  bnj168  34879  bnj529  34890  bnj906  35078  bnj970  35095  exdifsn  35227  cusgredgex2  35311  subfacp1lem5  35372  cvmsi  35453  cvmsval  35454  cvmsdisj  35458  cvmscld  35461  cvmsss2  35462  satfv1lem  35550  sinccvglem  35860  circum  35862  mpomulnzcnf  36487  unbdqndv2lem2  36768  bj-0int  37411  lindsadd  37925  lindsenlbs  37927  matunitlindflem2  37929  matunitlindf  37930  poimirlem6  37938  poimirlem7  37939  poimirlem8  37940  poimirlem16  37948  poimirlem18  37950  poimirlem19  37951  poimirlem21  37953  poimirlem22  37954  poimirlem24  37956  poimirlem25  37957  poimirlem26  37958  poimirlem27  37959  itg2addnclem2  37984  sdclem1  38055  rrncmslem  38144  rrnequiv  38147  isdrngo2  38270  isdrngo3  38271  eldmxrncnvepres  38746  eldmxrncnvepres2  38747  prtlem100  39296  prter2  39318  prter3  39319  lsatlspsn2  39429  lsateln0  39432  lsatn0  39436  lsatspn0  39437  lsatcmp  39440  lsatelbN  39443  islshpat  39454  lsat0cv  39470  lkrlspeqN  39608  dvheveccl  41549  dihlatat  41774  dochnel  41830  dihjat1  41866  dvh4dimlem  41880  dochsnkr2cl  41911  dochkr1  41915  dochkr1OLDN  41916  lcfl6lem  41935  lcfl9a  41942  lclkrlem2l  41955  lclkrlem2o  41958  lclkrlem2q  41960  lcfrlem9  41987  lcfrlem16  41995  lcfrlem17  41996  lcfrlem27  42006  lcfrlem37  42016  lcfrlem38  42017  lcfrlem40  42019  lcdlkreqN  42059  mapdrvallem2  42082  mapdn0  42106  mapdpglem20  42128  mapdpglem30  42139  mapdindp0  42156  mapdhcl  42164  mapdh6aN  42172  mapdh6dN  42176  mapdh6eN  42177  mapdh6kN  42183  mapdh8  42225  hdmap1l6a  42246  hdmap1l6d  42250  hdmap1l6e  42251  hdmap1l6k  42257  hdmapval3N  42275  hdmap10  42277  hdmap11lem2  42279  hdmapnzcl  42282  hdmaprnlem3eN  42295  hdmaprnlem17N  42300  hdmap14lem4a  42308  hdmap14lem7  42311  hdmap14lem14  42318  hgmaprnlem5N  42337  hdmaplkr  42350  hdmapip0  42352  hgmapvvlem2  42361  hgmapvvlem3  42362  hgmapvv  42363  redvmptabs  42791  readvrec2  42792  readvrec  42793  fiabv  42980  fsuppind  43022  0prjspnlem  43055  pellexlem5  43264  dfac11  43493  dfacbasgrp  43539  dgraalem  43576  dgraaub  43579  aaitgo  43593  proot1ex  43627  deg1mhm  43631  ofdivrec  44756  ofdivcan4  44757  ofdivdiv2  44758  expgrowth  44765  binomcxplemnotnn0  44786  dvdivbd  46355  dvdivcncf  46359  dirkeritg  46534  fourierdlem39  46578  fourierdlem57  46595  fourierdlem58  46596  fourierdlem59  46597  fourierdlem68  46606  fourierdlem76  46614  fourierdlem103  46641  fourierdlem104  46642  fourierdlem111  46649  setsnidel  47811  sprvalpwn0  47917  odz2prm2pw  47997  fmtnoprmfac1  47999  fmtnoprmfac2  48001  sfprmdvdsmersenne  48037  lighneallem2  48040  lighneallem3  48041  lighneal  48045  oddprmALTV  48121  evenprm2  48148  oddprmne2  48149  odd2prm2  48152  even3prm2  48153  isubgruhgr  48302  grimuhgr  48321  2zrngnmrid  48690  lincext1  48888  lindslinindsimp2lem5  48896  rege1logbrege0  48992  fllogbd  48994  relogbmulbexp  48995  relogbdivb  48996  nnpw2blen  49014  blennngt2o2  49026  blennn0e2  49028  dignn0ldlem  49036  line  49166  rrxline  49168  aacllem  50234