Theorem eldifsn 4717

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 395   ∈ wcel 2108   ≠ wne 2942   ∖ cdif 3880  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-v 3424  df-dif 3886  df-sn 4559

This theorem is referenced by:  elpwdifsn  4719  eldifsni  4720  rexdifsn  4724  raldifsni  4725  eldifvsn  4727  difsn  4728  prproe  4834  sossfld  6078  tpres  7058  onmindif2  7634  mptsuppd  7974  suppssr  7983  suppssov1  7985  suppsssn  7988  suppssfv  7989  dif1o  8292  difsnen  8794  limenpsi  8888  frfi  8989  fofinf1o  9024  en2eleq  9695  en2other2  9696  dfac8clem  9719  acni2  9733  acndom  9738  acnnum  9739  dfac9  9823  dfacacn  9828  kmlem3  9839  kmlem4  9840  fin23lem21  10026  canthp1lem2  10340  elni  10563  mulnzcnopr  11551  divval  11565  elnnne0  12177  elq  12619  rpcndif0  12678  modfzo0difsn  13591  modsumfzodifsn  13592  expcl2lem  13722  expclzlem  13734  hashdifpr  14058  hashgt23el  14067  prprrab  14115  hashle2prv  14120  reccn2  15234  rlimdiv  15285  eff2  15736  tanval  15765  rpnnen2lem9  15859  fzo0dvdseq  15960  oddprmgt2  16332  oddprmdvds  16532  4sqlem19  16592  prmlem0  16735  prmlem1a  16736  setsnid  16838  setsnidOLD  16839  grpinvnzcl  18562  symgextf  18940  f1omvdmvd  18966  pmtrprfv  18976  odcau  19124  efgsf  19250  efgsrel  19255  efgs1  19256  efgs1b  19257  efgsp1  19258  efgsres  19259  efgredlema  19261  efgredlemd  19265  efgrelexlemb  19271  gsumpt  19478  dmdprdd  19517  dprdcntz  19526  dprdfeq0  19540  dprd2da  19560  drngunit  19911  isdrng2  19916  drngid2  19922  isdrngd  19931  issubdrg  19964  sdrgacs  19984  cntzsdrg  19985  abvtriv  20016  islss  20111  lssneln0  20129  lssssr  20130  lbsind  20257  lbspss  20259  lspabs3  20298  lspsneq  20299  lspfixed  20305  lspexch  20306  islbs2  20331  isdomn2  20483  domnrrg  20484  cnflddiv  20540  cnfldinv  20541  xrs1mnd  20548  xrs10  20549  xrge0subm  20551  cnsubdrglem  20561  cnmgpid  20572  cnmsubglem  20573  gzrngunit  20576  zringunit  20600  zringndrg  20602  domnchr  20648  cnmsgngrp  20696  psgninv  20699  psgndiflemB  20717  lindfind  20933  lindsind  20934  lindff1  20937  lindfrn  20938  mvrcl  21131  coe1tmmul2  21357  mdetunilem9  21677  maducoeval2  21697  gsummatr01lem4  21715  ist1-2  22406  cmpfi  22467  2ndcdisj  22515  2ndcsep  22518  locfincmp  22585  alexsublem  23103  cldsubg  23170  imasdsf1olem  23434  prdsxmslem2  23591  reperflem  23887  xrge0gsumle  23902  xrge0tsms  23903  divcn  23937  evth  24028  cvsdiv  24201  cvsdivcl  24202  cphreccllem  24247  bcthlem5  24397  itg11  24760  i1fmullem  24763  i1fadd  24764  itg1addlem2  24766  i1fmulc  24773  itg1mulc  24774  ellimc3  24948  limcmpt2  24953  dvlem  24965  dvidlem  24984  dvcnp  24988  dvcobr  25015  dvrec  25024  dvrecg  25042  dvmptdiv  25043  dvcnvlem  25045  dvexp3  25047  dveflem  25048  dvferm1lem  25053  dvferm2lem  25055  lhop1lem  25082  ftc1lem5  25109  mdegleb  25134  coe1mul3  25169  ply1nz  25191  fta1blem  25238  fta1b  25239  ig1peu  25241  ig1pdvds  25246  plyeq0lem  25276  dgrub  25300  quotval  25357  fta1lem  25372  fta1  25373  elqaalem3  25386  qaa  25388  iaa  25390  aareccl  25391  aannenlem2  25394  abelthlem8  25503  abelth  25505  eff1olem  25609  logrncl  25628  eflog  25637  logeftb  25644  logdmss  25702  dvlog  25711  logbcl  25822  logbid1  25823  logb1  25824  elogb  25825  logbchbase  25826  relogbval  25827  relogbcl  25828  relogbreexp  25830  relogbmul  25832  nnlogbexp  25836  relogbcxp  25840  cxplogb  25841  relogbcxpb  25842  logbf  25844  logblog  25847  2logb9irrALT  25853  sqrt2cxp2logb9e3  25854  angval  25856  dcubic  25901  rlimcnp  26020  efrlim  26024  logexprlim  26278  dchrghm  26309  dchrabs  26313  lgsfcl2  26356  lgsval2lem  26360  lgsval3  26368  lgsmod  26376  lgsdirprm  26384  lgsne0  26388  gausslemma2dlem0f  26414  lgsquad2lem2  26438  2lgsoddprm  26469  2sqlem11  26482  2sqblem  26484  dchrvmaeq0  26557  rpvmasum2  26565  dchrisum0re  26566  qrngdiv  26677  tglngval  26816  tgisline  26892  axlowdimlem9  27221  axlowdimlem12  27224  axlowdimlem13  27225  elntg2  27256  upgrbi  27366  upgr1elem  27385  umgrislfupgrlem  27395  edgupgr  27407  subgruhgredgd  27554  upgrreslem  27574  nbgrel  27610  nbupgr  27614  nbupgrel  27615  nbumgrvtx  27616  nbgrssovtx  27631  nbupgrres  27634  nbusgrvtxm1uvtx  27675  nbupgruvtxres  27677  iscplgredg  27687  cusgredg  27694  cusgrfilem2  27726  usgredgsscusgredg  27729  1loopgrnb0  27772  1egrvtxdg0  27781  uhgrvd00  27804  vtxdginducedm1lem4  27812  eupth2lem3lem3  28495  frcond1  28531  frcond4  28535  2pthfrgr  28549  3cyclfrgrrn1  28550  n4cyclfrgr  28556  frgrwopreglem4a  28575  numclwwlk5  28653  ressupprn  30926  suppss3  30961  xdivval  31095  xrge0tsmsd  31219  pmtrcnel  31260  pmtrcnelor  31262  0nellinds  31468  extdg1id  31640  submatminr1  31662  ordtconnlem1  31776  ispisys2  32021  sigapisys  32023  sibfinima  32206  sseqf  32259  signswch  32440  signstfvn  32448  signsvtn0  32449  signstfvneq0  32451  signstfvcl  32452  signstfveq0a  32455  signstfveq0  32456  signsvfn  32461  signsvtp  32462  signsvtn  32463  signsvfpn  32464  signsvfnn  32465  signlem0  32466  bnj158  32608  bnj168  32609  bnj529  32621  bnj906  32810  bnj970  32827  exdifsn  32953  cusgredgex2  32984  subfacp1lem5  33046  cvmsi  33127  cvmsval  33128  cvmsdisj  33132  cvmscld  33135  cvmsss2  33136  satfv1lem  33224  sinccvglem  33530  circum  33532  xpord3ind  33727  addsval  34053  unbdqndv2lem2  34617  bj-0int  35199  lindsadd  35697  lindsenlbs  35699  matunitlindflem2  35701  matunitlindf  35702  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem16  35720  poimirlem18  35722  poimirlem19  35723  poimirlem21  35725  poimirlem22  35726  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  itg2addnclem2  35756  sdclem1  35828  rrncmslem  35917  rrnequiv  35920  isdrngo2  36043  isdrngo3  36044  prtlem100  36800  prter2  36822  prter3  36823  lsatlspsn2  36933  lsateln0  36936  lsatn0  36940  lsatspn0  36941  lsatcmp  36944  lsatelbN  36947  islshpat  36958  lsat0cv  36974  lkrlspeqN  37112  dvheveccl  39053  dihlatat  39278  dochnel  39334  dihjat1  39370  dvh4dimlem  39384  dochsnkr2cl  39415  dochkr1  39419  dochkr1OLDN  39420  lcfl6lem  39439  lcfl9a  39446  lclkrlem2l  39459  lclkrlem2o  39462  lclkrlem2q  39464  lcfrlem9  39491  lcfrlem16  39499  lcfrlem17  39500  lcfrlem27  39510  lcfrlem37  39520  lcfrlem38  39521  lcfrlem40  39523  lcdlkreqN  39563  mapdrvallem2  39586  mapdn0  39610  mapdpglem20  39632  mapdpglem30  39643  mapdindp0  39660  mapdhcl  39668  mapdh6aN  39676  mapdh6dN  39680  mapdh6eN  39681  mapdh6kN  39687  mapdh8  39729  hdmap1l6a  39750  hdmap1l6d  39754  hdmap1l6e  39755  hdmap1l6k  39761  hdmapval3N  39779  hdmap10  39781  hdmap11lem2  39783  hdmapnzcl  39786  hdmaprnlem3eN  39799  hdmaprnlem17N  39804  hdmap14lem4a  39812  hdmap14lem7  39815  hdmap14lem14  39822  hgmaprnlem5N  39841  hdmaplkr  39854  hdmapip0  39856  hgmapvvlem2  39865  hgmapvvlem3  39866  hgmapvv  39867  fsuppind  40202  0prjspnlem  40381  pellexlem5  40571  dfac11  40803  dfacbasgrp  40849  dgraalem  40886  dgraaub  40889  aaitgo  40903  proot1ex  40942  isdomn3  40945  deg1mhm  40948  ofdivrec  41833  ofdivcan4  41834  ofdivdiv2  41835  expgrowth  41842  binomcxplemnotnn0  41863  dvdivbd  43354  dvdivcncf  43358  dirkeritg  43533  fourierdlem39  43577  fourierdlem57  43594  fourierdlem58  43595  fourierdlem59  43596  fourierdlem68  43605  fourierdlem76  43613  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  setsnidel  44717  sprvalpwn0  44823  odz2prm2pw  44903  fmtnoprmfac1  44905  fmtnoprmfac2  44907  sfprmdvdsmersenne  44943  lighneallem2  44946  lighneallem3  44947  lighneal  44951  oddprmALTV  45027  evenprm2  45054  oddprmne2  45055  odd2prm2  45058  even3prm2  45059  2zrngnmrid  45396  lincext1  45683  lindslinindsimp2lem5  45691  rege1logbrege0  45792  fllogbd  45794  relogbmulbexp  45795  relogbdivb  45796  nnpw2blen  45814  blennngt2o2  45826  blennn0e2  45828  dignn0ldlem  45836  line  45966  rrxline  45968  aacllem  46391