Theorem eldifsn 4735

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2111   ≠ wne 2928   ∖ cdif 3894  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-sn 4574

This theorem is referenced by:  eldifsnd  4736  elpwdifsn  4738  eldifsni  4739  rexdifsn  4743  raldifsni  4744  eldifvsn  4746  difsn  4747  sossfld  6133  tpres  7135  onmindif2  7740  xpord3pred  8082  xpord3inddlem  8084  mptsuppd  8117  suppssr  8125  suppssov1  8127  suppssov2  8128  suppsssn  8131  suppssfv  8132  dif1o  8415  difsnen  8972  limenpsi  9065  frfi  9169  fofinf1o  9216  en2eleq  9899  en2other2  9900  dfac8clem  9923  acni2  9937  acndom  9942  acnnum  9943  dfac9  10028  dfacacn  10033  kmlem3  10044  kmlem4  10045  fin23lem21  10230  canthp1lem2  10544  elni  10767  mulnzcnf  11763  divval  11778  elnnne0  12395  elq  12848  rpcndif0  12911  modfzo0difsn  13850  modsumfzodifsn  13851  expcl2lem  13980  expclzlem  13990  hashdifpr  14322  hashgt23el  14331  prprrab  14380  hashle2prv  14385  reccn2  15504  rlimdiv  15553  eff2  16008  tanval  16037  rpnnen2lem9  16131  fzo0dvdseq  16234  oddprmgt2  16610  oddprmdvds  16815  4sqlem19  16875  prmlem0  17017  prmlem1a  17018  setsnid  17119  grpinvnzcl  18924  symgextf  19329  f1omvdmvd  19355  pmtrprfv  19365  odcau  19516  efgsf  19641  efgsrel  19646  efgs1  19647  efgs1b  19648  efgsp1  19649  efgsres  19650  efgredlema  19652  efgredlemd  19656  efgrelexlemb  19662  gsumpt  19874  dmdprdd  19913  dprdcntz  19922  dprdfeq0  19936  dprd2da  19956  isdomn2OLD  20627  domnrrg  20628  isdomn3  20630  drngunit  20649  isdrng2  20658  drngmcl  20665  drngid2  20667  isdrngd  20680  isdrngdOLD  20682  issubdrg  20695  sdrgacs  20716  cntzsdrg  20717  islss  20867  lssneln0  20886  lssssr  20887  lbsind  21014  lbspss  21016  lspabs3  21058  lspsneq  21059  lspfixed  21065  lspexch  21066  islbs2  21091  cnflddivOLD  21338  cnfldinv  21339  cnsubdrglem  21355  cnmgpid  21366  cnmsubglem  21367  gzrngunit  21370  xrs1mnd  21377  xrs10  21378  xrge0subm  21380  zringunit  21403  zringndrg  21405  domnchr  21469  cnmsgngrp  21516  psgninv  21519  psgndiflemB  21537  lindfind  21753  lindsind  21754  lindff1  21757  lindfrn  21758  mvrcl  21929  coe1tmmul2  22190  mdetunilem9  22535  maducoeval2  22555  gsummatr01lem4  22573  ist1-2  23262  cmpfi  23323  2ndcdisj  23371  2ndcsep  23374  locfincmp  23441  alexsublem  23959  cldsubg  24026  imasdsf1olem  24288  prdsxmslem2  24444  reperflem  24734  xrge0gsumle  24749  xrge0tsms  24750  divcnOLD  24784  divcn  24786  evth  24885  cvsdiv  25059  cvsdivcl  25060  cphreccllem  25105  bcthlem5  25255  itg11  25619  i1fmullem  25622  i1fadd  25623  itg1addlem2  25625  i1fmulc  25631  itg1mulc  25632  ellimc3  25807  limcmpt2  25812  dvlem  25824  dvidlem  25843  dvcnp  25847  dvcobr  25876  dvcobrOLD  25877  dvrec  25886  dvrecg  25904  dvmptdiv  25905  dvcnvlem  25907  dvexp3  25909  dveflem  25910  dvferm1lem  25915  dvferm2lem  25917  lhop1lem  25945  ftc1lem5  25974  mdegleb  25996  coe1mul3  26031  ply1nz  26054  fta1blem  26103  fta1b  26104  ig1peu  26107  ig1pdvds  26112  plyeq0lem  26142  dgrub  26166  quotval  26227  fta1lem  26242  fta1  26243  elqaalem3  26256  qaa  26258  iaa  26260  aareccl  26261  aannenlem2  26264  abelthlem8  26376  abelth  26378  eff1olem  26484  logrncl  26503  eflog  26512  logeftb  26519  logdmss  26578  dvlog  26587  logbcl  26704  logbid1  26705  logb1  26706  elogb  26707  logbchbase  26708  relogbval  26709  relogbcl  26710  relogbreexp  26712  relogbmul  26714  nnlogbexp  26718  relogbcxp  26722  cxplogb  26723  relogbcxpb  26724  logbf  26726  logblog  26729  2logb9irrALT  26735  sqrt2cxp2logb9e3  26736  angval  26738  dcubic  26783  rlimcnp  26902  efrlim  26906  efrlimOLD  26907  logexprlim  27163  dchrghm  27194  dchrabs  27198  lgsfcl2  27241  lgsval2lem  27245  lgsval3  27253  lgsmod  27261  lgsdirprm  27269  lgsne0  27273  gausslemma2dlem0f  27299  lgsquad2lem2  27323  2lgsoddprm  27354  2sqlem11  27367  2sqblem  27369  dchrvmaeq0  27442  rpvmasum2  27450  dchrisum0re  27451  qrngdiv  27562  addsval  27905  divsval  28128  elnns  28268  1nns  28277  tglngval  28529  tgisline  28605  axlowdimlem9  28928  axlowdimlem12  28931  axlowdimlem13  28932  elntg2  28963  upgrbi  29071  upgr1elem  29090  umgrislfupgrlem  29100  edgupgr  29112  subgruhgredgd  29262  upgrreslem  29282  nbgrel  29318  nbupgr  29322  nbupgrel  29323  nbumgrvtx  29324  nbgrssovtx  29339  nbupgrres  29342  nbusgrvtxm1uvtx  29383  nbupgruvtxres  29385  iscplgredg  29395  cusgredg  29402  cusgrfilem2  29435  usgredgsscusgredg  29438  1loopgrnb0  29481  1egrvtxdg0  29490  uhgrvd00  29513  vtxdginducedm1lem4  29521  eupth2lem3lem3  30210  frcond1  30246  frcond4  30250  2pthfrgr  30264  3cyclfrgrrn1  30265  n4cyclfrgr  30271  frgrwopreglem4a  30290  numclwwlk5  30368  ressupprn  32671  suppss3  32706  xdivval  32899  xrge0tsmsd  33042  pmtrcnel  33058  pmtrcnelor  33060  0nellinds  33335  dvdsruasso  33350  mxidlirredi  33436  extdg1id  33679  irngnzply1  33704  submatminr1  33823  ordtconnlem1  33937  ispisys2  34166  sigapisys  34168  sibfinima  34352  sseqf  34405  signswch  34574  signstfvn  34582  signsvtn0  34583  signstfvneq0  34585  signstfvcl  34586  signstfveq0a  34589  signstfveq0  34590  signsvfn  34595  signsvtp  34596  signsvtn  34597  signsvfpn  34598  signsvfnn  34599  signlem0  34600  bnj158  34741  bnj168  34742  bnj529  34753  bnj906  34942  bnj970  34959  exdifsn  35091  cusgredgex2  35167  subfacp1lem5  35228  cvmsi  35309  cvmsval  35310  cvmsdisj  35314  cvmscld  35317  cvmsss2  35318  satfv1lem  35406  sinccvglem  35716  circum  35718  mpomulnzcnf  36343  unbdqndv2lem2  36554  bj-0int  37145  lindsadd  37652  lindsenlbs  37654  matunitlindflem2  37656  matunitlindf  37657  poimirlem6  37665  poimirlem7  37666  poimirlem8  37667  poimirlem16  37675  poimirlem18  37677  poimirlem19  37678  poimirlem21  37680  poimirlem22  37681  poimirlem24  37683  poimirlem25  37684  poimirlem26  37685  poimirlem27  37686  itg2addnclem2  37711  sdclem1  37782  rrncmslem  37871  rrnequiv  37874  isdrngo2  37997  isdrngo3  37998  eldmxrncnvepres  38457  eldmxrncnvepres2  38458  prtlem100  38957  prter2  38979  prter3  38980  lsatlspsn2  39090  lsateln0  39093  lsatn0  39097  lsatspn0  39098  lsatcmp  39101  lsatelbN  39104  islshpat  39115  lsat0cv  39131  lkrlspeqN  39269  dvheveccl  41210  dihlatat  41435  dochnel  41491  dihjat1  41527  dvh4dimlem  41541  dochsnkr2cl  41572  dochkr1  41576  dochkr1OLDN  41577  lcfl6lem  41596  lcfl9a  41603  lclkrlem2l  41616  lclkrlem2o  41619  lclkrlem2q  41621  lcfrlem9  41648  lcfrlem16  41656  lcfrlem17  41657  lcfrlem27  41667  lcfrlem37  41677  lcfrlem38  41678  lcfrlem40  41680  lcdlkreqN  41720  mapdrvallem2  41743  mapdn0  41767  mapdpglem20  41789  mapdpglem30  41800  mapdindp0  41817  mapdhcl  41825  mapdh6aN  41833  mapdh6dN  41837  mapdh6eN  41838  mapdh6kN  41844  mapdh8  41886  hdmap1l6a  41907  hdmap1l6d  41911  hdmap1l6e  41912  hdmap1l6k  41918  hdmapval3N  41936  hdmap10  41938  hdmap11lem2  41940  hdmapnzcl  41943  hdmaprnlem3eN  41956  hdmaprnlem17N  41961  hdmap14lem4a  41969  hdmap14lem7  41972  hdmap14lem14  41979  hgmaprnlem5N  41998  hdmaplkr  42011  hdmapip0  42013  hgmapvvlem2  42022  hgmapvvlem3  42023  hgmapvv  42024  redvmptabs  42452  readvrec2  42453  readvrec  42454  fiabv  42628  fsuppind  42682  0prjspnlem  42715  pellexlem5  42925  dfac11  43154  dfacbasgrp  43200  dgraalem  43237  dgraaub  43240  aaitgo  43254  proot1ex  43288  deg1mhm  43292  ofdivrec  44418  ofdivcan4  44419  ofdivdiv2  44420  expgrowth  44427  binomcxplemnotnn0  44448  dvdivbd  46020  dvdivcncf  46024  dirkeritg  46199  fourierdlem39  46243  fourierdlem57  46260  fourierdlem58  46261  fourierdlem59  46262  fourierdlem68  46271  fourierdlem76  46279  fourierdlem103  46306  fourierdlem104  46307  fourierdlem111  46314  setsnidel  47476  sprvalpwn0  47582  odz2prm2pw  47662  fmtnoprmfac1  47664  fmtnoprmfac2  47666  sfprmdvdsmersenne  47702  lighneallem2  47705  lighneallem3  47706  lighneal  47710  oddprmALTV  47786  evenprm2  47813  oddprmne2  47814  odd2prm2  47817  even3prm2  47818  isubgruhgr  47967  grimuhgr  47986  2zrngnmrid  48355  lincext1  48554  lindslinindsimp2lem5  48562  rege1logbrege0  48658  fllogbd  48660  relogbmulbexp  48661  relogbdivb  48662  nnpw2blen  48680  blennngt2o2  48692  blennn0e2  48694  dignn0ldlem  48702  line  48832  rrxline  48834  aacllem  49901