Theorem eldifsn 4790

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 3972	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4644	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2975	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 574	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 275	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2105   ≠ wne 2937   ∖ cdif 3959  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-v 3479  df-dif 3965  df-sn 4631

This theorem is referenced by:  eldifsnd  4791  elpwdifsn  4793  eldifsni  4794  rexdifsn  4798  raldifsni  4799  eldifvsn  4801  difsn  4802  sossfld  6207  tpres  7220  onmindif2  7826  xpord3pred  8175  xpord3inddlem  8177  mptsuppd  8210  suppssr  8218  suppssov1  8220  suppssov2  8221  suppsssn  8224  suppssfv  8225  dif1o  8536  difsnen  9091  limenpsi  9190  frfi  9318  fofinf1o  9369  en2eleq  10045  en2other2  10046  dfac8clem  10069  acni2  10083  acndom  10088  acnnum  10089  dfac9  10174  dfacacn  10179  kmlem3  10190  kmlem4  10191  fin23lem21  10376  canthp1lem2  10690  elni  10913  mulnzcnf  11906  divval  11921  elnnne0  12537  elq  12989  rpcndif0  13051  modfzo0difsn  13980  modsumfzodifsn  13981  expcl2lem  14110  expclzlem  14120  hashdifpr  14450  hashgt23el  14459  prprrab  14508  hashle2prv  14513  reccn2  15629  rlimdiv  15678  eff2  16131  tanval  16160  rpnnen2lem9  16254  fzo0dvdseq  16356  oddprmgt2  16732  oddprmdvds  16936  4sqlem19  16996  prmlem0  17139  prmlem1a  17140  setsnid  17242  setsnidOLD  17243  grpinvnzcl  19041  symgextf  19449  f1omvdmvd  19475  pmtrprfv  19485  odcau  19636  efgsf  19761  efgsrel  19766  efgs1  19767  efgs1b  19768  efgsp1  19769  efgsres  19770  efgredlema  19772  efgredlemd  19776  efgrelexlemb  19782  gsumpt  19994  dmdprdd  20033  dprdcntz  20042  dprdfeq0  20056  dprd2da  20076  isdomn2OLD  20728  domnrrg  20729  isdomn3  20731  drngunit  20750  isdrng2  20759  drngmcl  20766  drngid2  20768  isdrngd  20781  isdrngdOLD  20783  issubdrg  20797  sdrgacs  20818  cntzsdrg  20819  islss  20949  lssneln0  20968  lssssr  20969  lbsind  21096  lbspss  21098  lspabs3  21140  lspsneq  21141  lspfixed  21147  lspexch  21148  islbs2  21173  cnflddivOLD  21431  cnfldinv  21432  xrs1mnd  21439  xrs10  21440  xrge0subm  21442  cnsubdrglem  21453  cnmgpid  21464  cnmsubglem  21465  gzrngunit  21468  zringunit  21494  zringndrg  21496  domnchr  21564  cnmsgngrp  21614  psgninv  21617  psgndiflemB  21635  lindfind  21853  lindsind  21854  lindff1  21857  lindfrn  21858  mvrcl  22029  coe1tmmul2  22294  mdetunilem9  22641  maducoeval2  22661  gsummatr01lem4  22679  ist1-2  23370  cmpfi  23431  2ndcdisj  23479  2ndcsep  23482  locfincmp  23549  alexsublem  24067  cldsubg  24134  imasdsf1olem  24398  prdsxmslem2  24557  reperflem  24853  xrge0gsumle  24868  xrge0tsms  24869  divcnOLD  24903  divcn  24905  evth  25004  cvsdiv  25178  cvsdivcl  25179  cphreccllem  25225  bcthlem5  25375  itg11  25739  i1fmullem  25742  i1fadd  25743  itg1addlem2  25745  i1fmulc  25752  itg1mulc  25753  ellimc3  25928  limcmpt2  25933  dvlem  25945  dvidlem  25964  dvcnp  25968  dvcobr  25997  dvcobrOLD  25998  dvrec  26007  dvrecg  26025  dvmptdiv  26026  dvcnvlem  26028  dvexp3  26030  dveflem  26031  dvferm1lem  26036  dvferm2lem  26038  lhop1lem  26066  ftc1lem5  26095  mdegleb  26117  coe1mul3  26152  ply1nz  26175  fta1blem  26224  fta1b  26225  ig1peu  26228  ig1pdvds  26233  plyeq0lem  26263  dgrub  26287  quotval  26348  fta1lem  26363  fta1  26364  elqaalem3  26377  qaa  26379  iaa  26381  aareccl  26382  aannenlem2  26385  abelthlem8  26497  abelth  26499  eff1olem  26604  logrncl  26623  eflog  26632  logeftb  26639  logdmss  26698  dvlog  26707  logbcl  26824  logbid1  26825  logb1  26826  elogb  26827  logbchbase  26828  relogbval  26829  relogbcl  26830  relogbreexp  26832  relogbmul  26834  nnlogbexp  26838  relogbcxp  26842  cxplogb  26843  relogbcxpb  26844  logbf  26846  logblog  26849  2logb9irrALT  26855  sqrt2cxp2logb9e3  26856  angval  26858  dcubic  26903  rlimcnp  27022  efrlim  27026  efrlimOLD  27027  logexprlim  27283  dchrghm  27314  dchrabs  27318  lgsfcl2  27361  lgsval2lem  27365  lgsval3  27373  lgsmod  27381  lgsdirprm  27389  lgsne0  27393  gausslemma2dlem0f  27419  lgsquad2lem2  27443  2lgsoddprm  27474  2sqlem11  27487  2sqblem  27489  dchrvmaeq0  27562  rpvmasum2  27570  dchrisum0re  27571  qrngdiv  27682  addsval  28009  divsval  28229  elnns  28357  1nns  28366  tglngval  28573  tgisline  28649  axlowdimlem9  28979  axlowdimlem12  28982  axlowdimlem13  28983  elntg2  29014  upgrbi  29124  upgr1elem  29143  umgrislfupgrlem  29153  edgupgr  29165  subgruhgredgd  29315  upgrreslem  29335  nbgrel  29371  nbupgr  29375  nbupgrel  29376  nbumgrvtx  29377  nbgrssovtx  29392  nbupgrres  29395  nbusgrvtxm1uvtx  29436  nbupgruvtxres  29438  iscplgredg  29448  cusgredg  29455  cusgrfilem2  29488  usgredgsscusgredg  29491  1loopgrnb0  29534  1egrvtxdg0  29543  uhgrvd00  29566  vtxdginducedm1lem4  29574  eupth2lem3lem3  30258  frcond1  30294  frcond4  30298  2pthfrgr  30312  3cyclfrgrrn1  30313  n4cyclfrgr  30319  frgrwopreglem4a  30338  numclwwlk5  30416  ressupprn  32704  suppss3  32741  xdivval  32885  xrge0tsmsd  33047  pmtrcnel  33091  pmtrcnelor  33093  0nellinds  33377  dvdsruasso  33392  mxidlirredi  33478  extdg1id  33690  irngnzply1  33705  submatminr1  33770  ordtconnlem1  33884  ispisys2  34133  sigapisys  34135  sibfinima  34320  sseqf  34373  signswch  34554  signstfvn  34562  signsvtn0  34563  signstfvneq0  34565  signstfvcl  34566  signstfveq0a  34569  signstfveq0  34570  signsvfn  34575  signsvtp  34576  signsvtn  34577  signsvfpn  34578  signsvfnn  34579  signlem0  34580  bnj158  34721  bnj168  34722  bnj529  34733  bnj906  34922  bnj970  34939  exdifsn  35071  cusgredgex2  35106  subfacp1lem5  35168  cvmsi  35249  cvmsval  35250  cvmsdisj  35254  cvmscld  35257  cvmsss2  35258  satfv1lem  35346  sinccvglem  35656  circum  35658  mpomulnzcnf  36281  unbdqndv2lem2  36492  bj-0int  37083  lindsadd  37599  lindsenlbs  37601  matunitlindflem2  37603  matunitlindf  37604  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem16  37622  poimirlem18  37624  poimirlem19  37625  poimirlem21  37627  poimirlem22  37628  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  itg2addnclem2  37658  sdclem1  37729  rrncmslem  37818  rrnequiv  37821  isdrngo2  37944  isdrngo3  37945  prtlem100  38840  prter2  38862  prter3  38863  lsatlspsn2  38973  lsateln0  38976  lsatn0  38980  lsatspn0  38981  lsatcmp  38984  lsatelbN  38987  islshpat  38998  lsat0cv  39014  lkrlspeqN  39152  dvheveccl  41094  dihlatat  41319  dochnel  41375  dihjat1  41411  dvh4dimlem  41425  dochsnkr2cl  41456  dochkr1  41460  dochkr1OLDN  41461  lcfl6lem  41480  lcfl9a  41487  lclkrlem2l  41500  lclkrlem2o  41503  lclkrlem2q  41505  lcfrlem9  41532  lcfrlem16  41540  lcfrlem17  41541  lcfrlem27  41551  lcfrlem37  41561  lcfrlem38  41562  lcfrlem40  41564  lcdlkreqN  41604  mapdrvallem2  41627  mapdn0  41651  mapdpglem20  41673  mapdpglem30  41684  mapdindp0  41701  mapdhcl  41709  mapdh6aN  41717  mapdh6dN  41721  mapdh6eN  41722  mapdh6kN  41728  mapdh8  41770  hdmap1l6a  41791  hdmap1l6d  41795  hdmap1l6e  41796  hdmap1l6k  41802  hdmapval3N  41820  hdmap10  41822  hdmap11lem2  41824  hdmapnzcl  41827  hdmaprnlem3eN  41840  hdmaprnlem17N  41845  hdmap14lem4a  41853  hdmap14lem7  41856  hdmap14lem14  41863  hgmaprnlem5N  41882  hdmaplkr  41895  hdmapip0  41897  hgmapvvlem2  41906  hgmapvvlem3  41907  hgmapvv  41908  redvmptabs  42368  readvrec2  42369  readvrec  42370  fiabv  42522  fsuppind  42576  0prjspnlem  42609  pellexlem5  42820  dfac11  43050  dfacbasgrp  43096  dgraalem  43133  dgraaub  43136  aaitgo  43150  proot1ex  43184  deg1mhm  43188  ofdivrec  44321  ofdivcan4  44322  ofdivdiv2  44323  expgrowth  44330  binomcxplemnotnn0  44351  dvdivbd  45878  dvdivcncf  45882  dirkeritg  46057  fourierdlem39  46101  fourierdlem57  46118  fourierdlem58  46119  fourierdlem59  46120  fourierdlem68  46129  fourierdlem76  46137  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  setsnidel  47301  sprvalpwn0  47407  odz2prm2pw  47487  fmtnoprmfac1  47489  fmtnoprmfac2  47491  sfprmdvdsmersenne  47527  lighneallem2  47530  lighneallem3  47531  lighneal  47535  oddprmALTV  47611  evenprm2  47638  oddprmne2  47639  odd2prm2  47642  even3prm2  47643  isubgruhgr  47791  grimuhgr  47815  2zrngnmrid  48099  lincext1  48299  lindslinindsimp2lem5  48307  rege1logbrege0  48407  fllogbd  48409  relogbmulbexp  48410  relogbdivb  48411  nnpw2blen  48429  blennngt2o2  48441  blennn0e2  48443  dignn0ldlem  48451  line  48581  rrxline  48583  aacllem  49031